我正在尝试学习使用 Isabelle/HOL。我想，“嘿，由一些开发它的人编写的教程会很棒”，所以看了看 https://isabelle.in.tum.de/doc/tutorial.pdf 其发布日期为 2018 年 8 月 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》中，有什么地方可以让我学会做最简单的事情吗？”
截至 2018 年，Isabelle 支持的唯一 IDE 是 Isabelle/jEdit，它包含在您可以从 Isabelle 网站下载的发行版中。有一个实验性 VSCode 插件正在积极开发中，但我建议暂时使用 Isabelle/jEdit。
您找到的教程在网站上列为“旧手册”之一。它在许多方面都严重过时，不应再使用。发布日期可能没有意义，因为它是生成 PDF 的日期，而不是编写文本的日期。有些人游说将该教程从网站上完全删除，而您的经验似乎证实我们确实应该这样做。
开始学习伊莎贝尔的最佳方法之一可能是书“具体语义”（提供免费在线版本）。它的前半部分基本上是对 Isabelle/HOL 的介绍，并有大量练习。 Isabelle网站上还有‘编程与证明’教程，和‘具体语义’的前半部分几乎一模一样。
但是，它侧重于计算机科学中的应用（编程语言的语义和一些函数式编程）。我不确定伊莎贝尔是否有关于如何做数学的好的教程；无论如何，对于初学者来说，数学在定理证明器中往往更难做，因为与非正式论文推理的差距更大。因此，即使您最终对形式化数学感兴趣，我也推荐“具体语义”。
顺便说一句：您提到了 Isabelle2017，但确实没有理由使用它来代替 Isabelle2018，这是撰写此答案时的最新版本。
最好的资源在这里： https://live.rbg.tum.de/course/2019/W/semantik
这是《伊莎贝尔》作者的视频讲座系列。他假设对 Haskel 等函数式编程有一定的了解。
此外，如果您遇到困难，只需将您的问题粘贴到此 Zulip 聊天中：https://isabelle.zulipchat.com/ 。他们响应迅速（几乎实时），因此您可以愉快地进行证明