Isabelle 中的 ML 编程：找不到某些内置函数和策略

Question

我正在研究“Isabelle Cookbook”以在 Isabelle 中编写 ML 代码。

不幸的是，许多示例都不起作用，因为没有找到内置函数（名称已更改？应该指定路径 structure.fct 吗？）。 例如，使用etac、rtac 和atac 的示例不再有效。新名称是什么？我如何自己找到它们？

Answer 1

伊莎贝尔食谱一直处于非官方状态，我怀疑它现在已经严重过时了。那里有一些不错的信息，但“官方”的最新来源是 Isabelle 实施手册。

要找出已重命名的事物的名称，查看 NEWS 文件通常很有用，例如在这种情况下：

* 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/tactic.ML 中找到它们。如果您正在寻找一些 ML 函数，只需搜索 ~~/src/Pure/ 目录，它们通常就在其中。 jEdit 的超级搜索对此特别有用。