伊莎贝尔的基础

Question

一年半前，我开始在 Isabelle 编写证明程序。那时我主要写 Isabelle/Isar 证明。最近，我一直在做一些 Isabelle/ML 级别的编程。我发现这篇描述 Isar 结构的博士论文非常鼓舞人心。我想知道是否有类似的来源可以了解 Isabelle 的基础。我在1989 年找到了这篇论文，在 1990 年找到了 Larry Paulson 的这篇论文。这是否描述了系统的当前基础？

更新：

我在Joshua Chen 的论文中找到了迄今为​​止对 Isabelle/Pure 最清楚的解释。关于内核如何隐藏定理创建有单独的关注。但这似乎是一种基于抽象数据类型的语言特性。

更新 2

在 Isabelle 的邮件列表的主题Explanation of derivation in Isabelle'sformal system下已经有一些讨论。指出的进一步参考是Isabelle/Isar implementation reference。这是上述博士论文的修订版。