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