Pureをいじっているが、性悪なシステムだな。 接頭辞PROPの意味が分からない。他の構文とは違う、かなり特殊。 型propには定数がなくて、true, falseもない。 PureとIFOLで関数適用の構文が違うのが非常にストレスだし、間違う。 prop型の定数はaxiomatizati…

情報検索の機能が低い。find_* とか print_* だけ。小洒落た機能はない。キーワード（コマンド名）に対して、そのコマンドがどのセオリーやどのMLファイルに由来するかも検索できないようだ。ディレクトリ内からファイルを探してソース読むしか無いようだ。s…

場合分けによる関数定義はどうするのか？ funとかの高級な方法使わないで。 項の計算（単純化）はどうするのか？ これもvalueとか使わずPureのレベルで。 定義（宣言）した型に対するユーザー定義の等号はどうやって定義するのか？

axiomatizationは、シグニチャ部と公理（の論理式）部からなる。IFOL.thy : axiomatization eq :: "['a, 'a] ⇒ o" (infixl "=" 50) where refl: "a = a" and subst: "a = b ==> P(a) ==> P(b)"構造は、localeやclassと同じだが、fixes/assumes ではなくて、…

fact(s) -- まだ謎。おそらくは、contextと同義。 constant -- 狭義の定数記号だけではなく、関数記号、関係記号、述語記号、定理に付けられたラベルなどは定数と呼ぶ。高階論理なので、関数、述語、関係なども意味領域のモノ（個体）となるから、定数と呼ん…