http://markun.cs.shinshu-u.ac.jp/kiso/projects/proofchecker/mizar/Mizar4/printout/mizar4ja_prn.pdf では、 vocabulary （単数？） notation （単数？） しかし、 Make Environment, Mizar Ver. 8.1.04 (Win32/FPC) Copyright (c) 1990-2015 Associatio…

http://markun.cs.shinshu-u.ac.jp/kiso/projects/proofchecker/mizar/Mizar4/printout/mizar4ja_prn.pdf では、 vocabulary （単数？） notation （単数？） constructors definitions theorems schemes requirements それ以外に次を確認している。 registr…

論理 Mizar ⊥ contradiction ¬φ not φ φ ∧ ψ φ & ψ φ ∨ ψ φ or ψ φ ⇒ ψ φ implies ψ φ ⇔ ψ φ iff ψ ∃ x. ψ ex x st ψ ∀ x. ψ for x holds ψ ∀ x.(φ ⇒ ψ) for x st φ holds ψ nonは形容詞の否定、andとsuch thatはスクリプト言語のキーワード。

Mizarでは同義語はほとんどない。beとbeing, hence（従って）、hereby（これによって）が次の意味。 then + thus = hence thus + now = hereby 英語としてはthus（よって）とhence（従って）はたいして差はない。

Nimに統一呼び出し構文というのがある。 http://nim-lang.org/docs/manual.html#procedures-method-call-syntax Eiffelでも、プロパティとメソッドをまとめてフィーチャと呼んでいて、プロパティと引数なしメソッドの区別はなかったと思う。

isar-refのp.46に書いてある話。コンテキストとは、処理系が持っている定理＆ルールのデータベースのことだとする。このコンテキストが見えないことがわかりにくさの大きな原因だ。さらに、コンテキストは入れ子になる。Isarでは、コンテキストを可視化する…

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 ではなくて、…