我想在一个名为理论的理论中定义我自己的列表类型List,但是已经存在一个具有该名称的理论.是否有比它更轻量级的理论Main？
请注意，$ISABELLE_HOME/src/HOL/ex/Seq.thy给出了一个定义您自己的列表数据类型以进行实验的最小示例，而没有着手解决如何在其Main入口点下方使用系统的微妙问题。（初学者会感到困惑，专家不会这样做。）
从理论上讲，您可以导入的最原始理论是Pure，但这只是基本的逻辑框架，还没有像 HOL 那样的任何对象逻辑。只是出于好奇，您可以查看从$ISABELLE_HOME/src/HOL/ex/Higher_Order_Logic.thy哪个开始Pure并在其上定义了一个最小版本的 HOL，但没有您期望从完整 Isabelle/HOL 中获得的任何高级理论和工具。
您无法在 Isabelle 中导入任何内容（因为即使对于基本逻辑，导入也是必要的）。Isabelle 中的 HOL 实现具有三个受支持的入口点：Main、Complex_Main（加上Main一些分析）和Plain，但只有前两个适合常规使用。
Plain 已经包含了基本逻辑，但在标准库方面几乎没有任何内容（例如没有列表）。但也缺少像 QuickCheck、Sledgehammer 和代码生成器这样的重要工具。此外，如果您从 Plain 开始，以便能够命名自己的理论列表，请注意您的理论将与基于 Main（几乎是所有内容）构建的任何工作不兼容。
所以，除非你有充分的理由这样做，否则我建议遵循拉斐尔的评论并给你的列表理论另一个名字。