どう違う？

print_options 便利。

http://isabelle.in.tum.de/library/HOL/HOL-Isar_Examples/outline.pdf では、 引用符をやめている。 ハイフンを名前に使っている。

オールドスタイルの証明コマンド／証明メソッドは、isar-refの"9.2 Basic proof tools"にある。

次は最初から使える。 typedecl 型または型構成子を導入できる。型レベルでの定数（＝型名）と定関数（＝型構成子）のシグネチャ宣言のようなもの。 class 型クラスは使える。「class 名前だけ」というのも特別にあって、これでユニバーサルな型クラスを定義…

lemmas（複数形！）というコマンドがある。lemmas G = A B C のように書いて、複数の定理をグルーピングできる。lemmas X = A なら、定理Aに別名Xを与えることが出来る。これを使うと、特定の名前Aの定理の内容を目視できる。ダミーの名前 X を使って、lemma…

シグネチャ（って言うかどうか知らんが）の宣言のとき、foo: "'a => 'a => X" (infix "$$" 70) のようにしてmixfix構文と優先度を指定できる。シグネチャで指定し忘れても、後からmixfixの宣言だけ出来る。 notation 名前 ( mixfix指定 )と書けばいい。mixfi…

definition はPureレベルで使える。definitionは定数定義、関数定義に使えるが、形式としては、等号的公理の追加になる。"左辺 == 右辺" で、「右辺により左辺が定義される」と読むようだ。左辺は定数、関数・演算子の呼び出し形式とか。書き換え規則を定義…

NGと書いてあるところだけダメ。 (* on top of Pure *) axiomatization A:: "'a ⇒ prop" and B:: "'a ⇒ prop" and P :: "prop" and Q :: "prop" term "op ==> P Q" term "P ==> Q" (* NG *) term "(A a)" term "(B b)" term "op ==> (A a) (B b)" term "(A a…

論理の説明が論理的にされることはほぼないので、用語法がイイカゲンで、曖昧・多義的・気分次第・行き当たりばったりであることはショーガナイとは思っているが、なんかガイドラインくらいは欲しい。どこにもガイドラインはない。自分で作ろう。多義的で注…

歴史を調べないと分からない処理系、てのも困ったもんだが、 エジンバラLFが「ロジカルフレーム」として先行か？ λPrologってのもある。 スコットのLCF理論が背景 ミルナーのMLで実装 CoqはIsabelleの後: Isabelle 1986年、Coq 1989年 3年後 [追記] "Logic o…