我正在学习《Isabelle Cookbook》，以便用 Isabelle 编写 ML 代码。
不幸的是，许多示例无法运行，因为找不到内置函数(名称已更改？应指定路径structure.fct？)。
例如，使用 etac、rtac 和 atac 的示例不再有效。新名称是什么？我如何自己找到它们？
最佳答案
伊莎贝尔食谱一直处于非常非官方的状态，我怀疑它现在已经严重过时了。那里有一些很好的信息，但“官方”的最新来源是 Isabelle 实现手册。
要找出已重命名的事物的名称，查看新闻文件通常很有用，例如在这种情况下:
* Old tactic shorthands atac, rtac, etac, dtac, ftac have been
discontinued. INCOMPATIBILITY, use regular assume_tac, resolve_tac etc.
instead (with proper context).
您可以在 ~~/src/Pure/tropic.ML 中找到这些内容。如果您正在寻找一些 ML 函数，只需搜索 ~~/src/Pure/ 目录，它们通常就在其中。 jEdit 的 super 搜索对此特别有用。
关于isabelle - Isabelle 中的 ML 编程 : could not find some of the built-in functions and tactics，我们在Stack Overflow上找到一个类似的问题： https://stackoverflow.com/questions/47214498/