0

我在学习伊莎贝尔的展开规则时遇到了一些问题。希望有人能解答，谢谢。

  1. 我需要导入 Isabella 的内置 HOL 库来引入一些已定义的量词。当我用Isabella2017打开%ISABELLE_HOME%\src\HOL\HOL.thy时，第七行“theory HOL”会报错“Cannot update finished theory"HOL.HOL"”。

  2. 你遇到过同样的问题吗？您是如何在 HOL 库中引入内置规则的？

4

0 回答 0