【发布时间】：2019-01-06 06:46:30
【问题描述】：
我在 Isabelle/HOL 中有一些定义和定理，需要在 HOL 中使用这些相同的定义和定理。手动翻译代码当然是可能的，但很麻烦。有没有（半）自动执行这种翻译的程序？
如果由于某种原因无法做到这一点，请解释原因，因为这对我来说是一项重要的学习。
【问题讨论】：
【发布时间】：2019-01-06 06:46:30
【问题描述】：
理论上，您应该能够轻松地在 HOL 实现之间移动定理和定义，这个想法是 OpenTheory 项目的动机。不幸的是，在实践中，Isabelle 的 HOL 实现与其他人有很大不同，并且根据 OpenTheory 页面，Isabelle 目前只能使用 OpenTheory 导入定理，而不能导出它们。
【讨论】：