在伊莎贝尔的编程:找不到一些内置的功能和策略。

Question

我正在学习"Isabelle Cookbook“，用Isabelle编写ML代码。

不幸的是，许多示例无法工作，因为没有找到内置函数(名称更改了吗？)应该指定路径structure.fct？)。例如，使用etac、rtac和atac的示例不再起作用。什么是新的名字，我如何找到他们自己？

Answer 1

伊莎贝尔食谱一直有一个非常非正式的地位，我怀疑它现在已经严重过时了。里面有一些很好的信息，但是最新的官方资料是伊莎贝尔的实现手册。

要查找已重命名的事物的名称，通常可以在新闻文件中查找，例如在本例中：

* 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的超搜索在这方面特别有用。