isabelle - 在 Isabelle 中探索 ML 文件

Question

我想知道在 Isabelle ML 文件中是否有一种方法可以激活普通理论文件所具有的功能，即您可以在定义中按下 Ctrl+单击鼠标并获得所需的定义。

但是，这似乎不适用于 ML 文件。我可以激活任何选项以从函数导航到其定义吗？

标签： isabellejedit

Answer 1

启用您寻求的功能的一种方法是将 ML 文件包含在*.thy带有命令的文件中，ML_file并在 jEdit 中打开它们。当然，可能存在更好的选择。