我想在一个名为List的理论中定义自己的列表类型，但是已经有了一个使用该名称的理论。
有没有比Main更轻量级的理论？
最佳答案
请注意，$ISABELLE_HOME/src/HOL/ex/Seq.thy提供了一个最小的示例来定义您自己的列表数据类型以进行实验，而无需着手讨论如何在Main入口点以下使用系统的棘手问题。 (初学者会感到困惑，而专家则不会这样做。)
从理论上讲，您可以导入的最原始的理论是Pure，但这只是基本的逻辑框架，还没有像HOL这样的任何对象逻辑。出于好奇，您可以查看$ISABELLE_HOME/src/HOL/ex/Higher_Order_Logic.thy，它从Pure开始，并定义了最低限度的H.O.L。最重要的是，它没有完整的Isabelle/HOL所期望的任何高级理论和工具。
关于isabelle - 可能不会在伊莎贝尔(Isabelle)中引入任何理论吗？，我们在Stack Overflow上找到一个类似的问题：https://stackoverflow.com/questions/11336535/