isabelle - 伊莎贝尔 2017 年——开始
问题描述
我正在尝试学习使用 Isabelle/HOL。我想，“嘿，由一些开发它的人写的教程会很棒”，所以看了 https://isabelle.in.tum.de/doc/tutorial.pdf ，它的发布日期是 8 月2018 年 1 月 15 日。不过，在尝试通过示例工作时，我在文本中发现了这样的内容：
“经典的 Isabelle 用户界面是 David Aspinall 的 Proof General / Emacs。这本书对 Proof General 的介绍很少，它有自己的文档。” （第三页）
“如果发生任何奇怪的事情，我们建议您通过 Proof General 菜单项 Isabelle > Settings > Show Types 让 Isabelle 显示所有类型信息（有关详细信息，请参阅第 1.5 节）。” （第 5 页）
问题是 Proof General 似乎不再适用于 Isabelle（请参阅Isabelle2016 和 Proof General）。我很困惑为什么教程会基于过时的软件，但我真正的问题是：
“在伊莎贝尔 2017 年，我有没有什么地方可以学习做最简单的事情？”