フラン人の名前、「ウエ」に聞こえる。ウエはポールソンの先輩らしく、イザベルはウエの娘さんだとか。

古色蒼然たる仕様、先進的、実験的、前衛的な試みの混合物、ごった煮風。十何年か前に「こりゃダメだ、生理的に受け付けない」と思った酷い構文も健在。ドキュメントがPDFで読みやすいが、PDFだけ。コマンドやキーワードによる検索が出来ないで不便。PDFの検…

この順で読むといいかも。 FOL/IFOL.thy ← Pure FOL/FOL.thy ← IFOL LCF/LCF.thy ← FOL CTT/CTT.thy ← Pure CTT/Bool.thy ← CTT CTT/Arith.thy ← Bool

axiomatization axiomはアを強くア!キシオム、axiomatizationは割と平板で、アキシオマタゼーションと聞こえる。アキシオマチゼーションじゃないな。ラテン語のaxiomataは、アキシオーマタ（秋し大ウ股）っぽい。

次が分かりやすいようだった、[追記]そうでもない→Tobias NipkowのIsar解説 - 檜山正幸のキマイラ飼育記 メモ編 [/追記] Title: A Tutorial Introduction to Structured Isar Proofs Author: Tobias Nipkow http://citeseerx.ist.psu.edu/viewdoc/download?d…

実に充実してるが、膨大でゲンナリ。 The Isabelle/Isar Reference Manual 341 pages The Isabelle/Isar Implementation 159 pages The Isabelle System Manual 40 pages Isabelle/jEdit 60 pages Programming and Proving in Isabelle/HOL 63 pages A Proof…