如何解决如何在 Isabelle 中编写扩展规则？
我在学习伊莎贝尔的展开规则时遇到了一些问题。希望有人能解答，谢谢。
-
我需要导入 Isabella 的内置 HOL 库来引入一些定义的量词。当我用Isabella2017打开%ISABELLE_HOME%\src\HOL\HOL.thy时，第七行“theory HOL”会报错“无法更新完成的理论“HOL.HOL””。
-
你遇到过同样的问题吗？你是如何引入 HOL 库中的内置规则的？
版权声明：本文内容由互联网用户自发贡献，该文观点与技术仅代表作者本人。本站仅提供信息存储空间服务，不拥有所有权，不承担相关法律责任。如发现本站有涉嫌侵权/违法违规的内容， 请发送邮件至 dio@foxmail.com 举报，一经查实，本站将立刻删除。
