「*⁄」OK、だが裏ワザ過ぎるよ 「*\/」ダメ、\/ がそのまま見える 「*/」ダメ、すべてそのまま見える 「*/」ダメ、すべてそのまま見える 「*\if\endif/」 OK 「*@if@endif/」 なぜかダメ 「*\」の2文字になる。たぶんバグ。

外部構文もセオリーで定義して拡張できる。valueは~~/src/HOL/Code_Evaluation.thyで定義されている。つまり、imports Code_Evaluation でvalueが利用可能となる。Pureだと、funもtermも使えない。

fun plus x y = x + y; (* OK *) val plus = fn x => fn y => x + y; (* OK *) val plus = fn (x, y) => x + y; (* OK *) val plus = fn x y => x + y; (* NG *) 最後がNGなのが納得がいかない！ が、そうなんだから仕方ない。最初のような書き方をするしか…

@attention と @warning があり、どちらもそれらしく表示されるが、使い分けがワカラン。まー、自分で決めるってことだろう。

https://www.it.uu.se/grad/courses/gc0910/isabelle/isar-overview.pdf あんまり分かりやすくない。説明がうまくないような。メタ論理（Pure）と対象論理のレベルと、自然演繹との関係が書いてない、つうか、書いたつもりになっているけど説明になってない…