イザベルでのMLプログラミング（初心者）

Question

私はイザベルでMLコードを書く方法を学んでいます。

「Isabelle Cookbook」（2013）およびIsabelle2017を使用した説明と例に従っています。

機能term_ofおよびprop_ofはもう使用できません。 MLエラーに12ページ弾力上昇に 例：

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

新機能は何ですか？

ありがとうございます。

Answer 1

これらの両方とも現在名前空間にする必要があります。Thm.prop_ofとThm.term_of。