我需要在一篇论文上做一个演示，该论文在某些时候使用了 Isabelle/Isar 和 Isabelle/HOL。
我尝试在网上搜索有关 Isabelle/HOL 和 Isabelle/Isar 的信息，以便能够在一两张幻灯片中说明这些关系。以下是我目前理解的关系：
- Isabelle - 为演绎系统提供通用基础架构
- 基于标准 ML 编程语言
- 提供了一个 IDE，允许您编写以后可以证明的理论。
- Isabelle/Pure - 根据此链接
的高阶逻辑的最小版本：
- 它是可以输入到 isabelle IDE 中的实际语言吗？
- 还是技术规范？
Isabelle/HOL（高阶逻辑）：
- 它是图书馆还是语言？
- 它与 Isabelle/Pure 有什么关系？
- 它本质上是程序性的吗？
- 战术只存在于 Isabelle/HOL 中吗？
- 是 LCF - 逻辑可交换函数吗？
伊莎贝尔/伊萨尔：
- 基于 Isabelle/Pure 的结构化证明语言
- 声明式
- 它是此处所述的 Isabelle/HOL 的扩展吗？
- 语言环境是否只存在于 Isabelle/Isar？
Isabelle/IDE 默认支持什么？
只是觉得我从不同的来源获得了相互矛盾的信息，并想解决这个问题。
提前致谢