1

目前，我有几个 HOL-light 格式的定理（连同证明），我想将它们转换成 Isabelle 格式的定理。我知道 OpenTheory ( http://www.gilith.com/opentheory/ ) 可以做到，但我不知道从哪里开始，因为我找不到任何可以参考的详细教程/示例。因此，我想知道从哪里开始可能是一个好点。提前非常感谢！

4

0 回答 0