Isabelleのドキュメント

実に充実してるが、膨大でゲンナリ。

1. The Isabelle/Isar Reference Manual 341 pages
2. The Isabelle/Isar Implementation 159 pages
3. The Isabelle System Manual 40 pages
4. Isabelle/jEdit 60 pages
5. Programming and Proving in Isabelle/HOL 63 pages
6. A Proof Assistant for Higher-Order Logic 223 pages
7. Picking Nits 53 pages
8. Code generation from Isabelle/HOL theories 43 pages
9. Defining (Co)datatypes and Primitively (Co)recursive Functions in Isabelle/HOL 61 pages

他にもイッパイ！ http://www.cl.cam.ac.uk/research/hvg/Isabelle/documentation.html

[追記]Isabelle/jEditからアクセス可能なものは 11 + 5 = 16文書：

1. What’s in Main 11 pages
2. LaTex Sugar for Isabelle Documents 11 pages
3. The Eisbach User Manual 26 pages
4. Hammering Away 27 pages
5. Defining Recursive Functions in Isabelle/HOL 20 pages
6. Haskell-style type classes with Isabelle/Isar 22 pages
7. Tutorial to Locales and Locale Interpretation 20 pages

総計で 1180 pages

[/追記]

[さらに追記]古い文書と言いながら、基礎的セオリーを読むには必須じゃん、コレ。

• Isabelle's Logics 99 pages
• Old Introduction to Isabelle 77 pages
• Isabelle’s Logics: FOL and ZF 85 pages

総計1441ページになった。

さらに追加

• jEdit 5.3 User's Guide 147 pages

1600ページ超えか。

[/さらに追記]