| author | wenzelm |
| Sat, 21 Jul 2012 22:13:50 +0200 | |
| changeset 49436 | c4d337782de4 |
| parent 49364 | a78e5d399599 |
| child 49473 | 09710d6fc3d1 |
| permissions | -rw-r--r-- |
| wenzelm@49364 | 1 |
session HOL! (1) in "." = Pure + |
| wenzelm@49353 | 2 |
description {* Classical Higher-order Logic *}
|
| wenzelm@49353 | 3 |
options [document_graph] |
| wenzelm@49353 | 4 |
theories Complex_Main |
| wenzelm@49353 | 5 |
files "document/root.tex" "document/root.bib" |
| wenzelm@49353 | 6 |
|
| wenzelm@49353 | 7 |
session "HOL-Base"! in "." = Pure + |
| wenzelm@49353 | 8 |
description {* Raw HOL base, with minimal tools *}
|
| wenzelm@49353 | 9 |
options [document = false] |
| wenzelm@49353 | 10 |
theories HOL |
| wenzelm@49353 | 11 |
|
| wenzelm@49353 | 12 |
session "HOL-Plain"! in "." = Pure + |
| wenzelm@49353 | 13 |
description {* HOL side-entry after bootstrap of many tools and packages *}
|
| wenzelm@49353 | 14 |
options [document = false] |
| wenzelm@49353 | 15 |
theories Plain |
| wenzelm@49353 | 16 |
|
| wenzelm@49353 | 17 |
session "HOL-Main"! in "." = Pure + |
| wenzelm@49353 | 18 |
description {* HOL side-entry for Main only, without Complex_Main *}
|
| wenzelm@49353 | 19 |
options [document = false] |
| wenzelm@49353 | 20 |
theories Main |
| wenzelm@49353 | 21 |
|
| wenzelm@49364 | 22 |
session "HOL-Proofs"! (2) in "." = Pure + |
| wenzelm@49353 | 23 |
description {* HOL-Main with proof terms *}
|
| wenzelm@49436 | 24 |
options [document = false, proofs = 2, parallel_proofs = 0] |
| wenzelm@49353 | 25 |
theories Main |
| wenzelm@49353 | 26 |
|
| wenzelm@49364 | 27 |
session HOLCF! (3) = HOL + |
| wenzelm@49353 | 28 |
description {*
|
| wenzelm@49353 | 29 |
Author: Franz Regensburger |
| wenzelm@49353 | 30 |
Author: Brian Huffman |
| wenzelm@49353 | 31 |
|
| wenzelm@49353 | 32 |
HOLCF -- a semantic extension of HOL by the LCF logic. |
| wenzelm@49353 | 33 |
*} |
| wenzelm@49353 | 34 |
options [document_graph] |
| wenzelm@49353 | 35 |
theories [document = false] |
| wenzelm@49353 | 36 |
"~~/src/HOL/Library/Nat_Bijection" |
| wenzelm@49353 | 37 |
"~~/src/HOL/Library/Countable" |
| wenzelm@49353 | 38 |
theories Plain_HOLCF Fixrec HOLCF |
| wenzelm@49353 | 39 |
files "document/root.tex" |
| wenzelm@49353 | 40 |