1 session HOL! (1) in "." = Pure +
2 description {* Classical Higher-order Logic *}
3 options [document_graph]
5 files "document/root.tex" "document/root.bib"
7 session "HOL-Base"! in "." = Pure +
8 description {* Raw HOL base, with minimal tools *}
9 options [document = false]
12 session "HOL-Plain"! in "." = Pure +
13 description {* HOL side-entry after bootstrap of many tools and packages *}
14 options [document = false]
17 session "HOL-Main"! in "." = Pure +
18 description {* HOL side-entry for Main only, without Complex_Main *}
19 options [document = false]
22 session "HOL-Proofs"! (2) in "." = Pure +
23 description {* HOL-Main with proof terms *}
24 options [document = false, proofs = 2, parallel_proofs = 0]
27 session HOLCF! (3) = HOL +
29 Author: Franz Regensburger
32 HOLCF -- a semantic extension of HOL by the LCF logic.
34 options [document_graph]
35 theories [document = false]
36 "~~/src/HOL/Library/Nat_Bijection"
37 "~~/src/HOL/Library/Countable"
38 theories Plain_HOLCF Fixrec HOLCF
39 files "document/root.tex"