--- a/src/HOL/ROOT Wed Mar 13 17:06:45 2013 +0100
+++ b/src/HOL/ROOT Wed Mar 13 17:13:22 2013 +0100
@@ -1,7 +1,9 @@
chapter HOL
session HOL (main) = Pure +
- description {* Classical Higher-order Logic *}
+ description {*
+ Classical Higher-order Logic.
+ *}
options [document_graph]
theories Complex_Main
files
@@ -11,7 +13,9 @@
"document/root.tex"
session "HOL-Proofs" = Pure +
- description {* HOL-Main with explicit proof terms *}
+ description {*
+ HOL-Main with explicit proof terms.
+ *}
options [document = false, proofs = 2]
theories Main
files
@@ -19,7 +23,9 @@
"Tools/Quickcheck/PNF_Narrowing_Engine.hs"
session "HOL-Library" (main) in Library = HOL +
- description {* Classical Higher-order Logic -- batteries included *}
+ description {*
+ Classical Higher-order Logic -- batteries included.
+ *}
theories
Library
(*conflicting type class instantiations*)
@@ -264,7 +270,9 @@
files "document/root.bib" "document/root.tex"
session "HOL-Auth" in Auth = HOL +
- description {* A new approach to verifying authentication protocols. *}
+ description {*
+ A new approach to verifying authentication protocols.
+ *}
options [document_graph]
theories
Auth_Shared
@@ -346,7 +354,9 @@
theories Hilbert_Classical
session "HOL-Proofs-Extraction" in "Proofs/Extraction" = "HOL-Proofs" +
- description {* Examples for program extraction in Higher-Order Logic *}
+ description {*
+ Examples for program extraction in Higher-Order Logic.
+ *}
options [condition = ISABELLE_POLYML, proofs = 2, parallel_proofs = 0]
theories [document = false]
"~~/src/HOL/Library/Code_Target_Numeral"
@@ -471,7 +481,9 @@
files "document/root.tex"
session "HOL-ex" in ex = HOL +
- description {* Miscellaneous examples for Higher-Order Logic. *}
+ description {*
+ Miscellaneous examples for Higher-Order Logic.
+ *}
options [timeout = 3600, condition = ISABELLE_POLYML]
theories [document = false]
"~~/src/HOL/Library/State_Monad"
@@ -669,12 +681,16 @@
theories [quick_and_dirty] VC_Condition
session "HOL-Cardinals-Base" in Cardinals = HOL +
- description {* Ordinals and Cardinals, Base Theories *}
+ description {*
+ Ordinals and Cardinals, Base Theories.
+ *}
options [document = false]
theories Cardinal_Arithmetic
session "HOL-Cardinals" in Cardinals = "HOL-Cardinals-Base" +
- description {* Ordinals and Cardinals, Full Theories *}
+ description {*
+ Ordinals and Cardinals, Full Theories.
+ *}
options [document = false]
theories Cardinals
files
@@ -683,17 +699,23 @@
"document/root.bib"
session "HOL-BNF-LFP" in BNF = "HOL-Cardinals-Base" +
- description {* Bounded Natural Functors for Datatypes *}
+ description {*
+ Bounded Natural Functors for Datatypes.
+ *}
options [document = false]
theories BNF_LFP
session "HOL-BNF" in BNF = "HOL-Cardinals" +
- description {* Bounded Natural Functors for (Co)datatypes *}
+ description {*
+ Bounded Natural Functors for (Co)datatypes.
+ *}
options [document = false]
theories BNF
session "HOL-BNF-Examples" in "BNF/Examples" = "HOL-BNF" +
- description {* Examples for Bounded Natural Functors *}
+ description {*
+ Examples for Bounded Natural Functors.
+ *}
options [document = false]
theories
Lambda_Term
@@ -720,7 +742,9 @@
files "document/root.tex"
session "HOL-NSA" in NSA = HOL +
- description {* Nonstandard analysis. *}
+ description {*
+ Nonstandard analysis.
+ *}
options [document_graph]
theories Hypercomplex
files "document/root.tex"
@@ -958,7 +982,9 @@
files "document/root.tex"
session "HOLCF-ex" in "HOLCF/ex" = HOLCF +
- description {* Misc HOLCF examples *}
+ description {*
+ Miscellaneous examples for HOLCF.
+ *}
options [document = false]
theories
Dnat
@@ -1046,7 +1072,9 @@
TrivEx2
session "HOL-Datatype_Benchmark" in Datatype_Benchmark = HOL +
- description {* Some rather large datatype examples (from John Harrison). *}
+ description {*
+ Some rather large datatype examples (from John Harrison).
+ *}
options [document = false]
theories [condition = ISABELLE_FULL_TEST, timing]
Brackin
@@ -1055,7 +1083,9 @@
Verilog
session "HOL-Record_Benchmark" in Record_Benchmark = HOL +
- description {* Some benchmark on large record. *}
+ description {*
+ Some benchmark on large record.
+ *}
options [document = false]
theories [condition = ISABELLE_FULL_TEST, timing]
Record_Benchmark