我在 Isabelle/HOL 中有一些定义和定理，需要在 HOL 中使用这些相同的定义和定理。手动翻译代码当然是可能的，但很麻烦。有没有（半）自动执行这种翻译的程序？
如果由于某种原因这是不可能的，请解释原因，因为这对我来说是一个重要的学习。
问问题
125 次
1 回答
3
从理论上讲，您应该能够轻松地在 HOL 实现之间移动定理和定义，这个想法是OpenTheory项目的动机。不幸的是，在实践中，Isabelle 的 HOL 实现与其他实现有很大不同，并且根据 OpenTheory 页面，Isabelle 目前只能使用 OpenTheory 导入定理，而不能导出它们。
于 2018-07-30T11:34:16.823 回答