小编Q.Y*_*ang的帖子

在 Isabelle 中，命令print_state可以打印需要证明的当前目标。但是，我希望以其他易于处理的格式打印目标，例如 S 表达式和抽象语法树。

默认打印模式不包括这种格式，所以我想知道如何修改Isabelle内部的ML文件。或者更具体地说，当前目标如何通过打印。我很高兴它在 ML 文件中是 AST 格式，然后才被传递到打印，但我很难找到变量是如何传输的。有谁知道如何解决这个问题？

例如，Isabelle 可以将“and”表示为“^”，“or”表示为“v”……有没有办法获得所有这些类型的运算符/构造函数的完整列表？