在Isabelle中编程(初学者)

Question

我正在学习如何用Isabelle编写ML代码(刚刚开始)。

我遵循“伊莎贝尔食谱”(2013年)中的解释和例子，并使用Isabelle2017。

term_of和prop_of函数不能再使用了？第12页中的示例导致ML错误：

ML error⌂:
Value or constructor (prop_of) has not been declared

新功能是什么？

谢谢。

Answer 1

这两者现在都需要命名空间：Thm.prop_of和Thm.term_of。