--- a/src/HOL/ROOT Tue Aug 28 17:17:25 2012 +0200
+++ b/src/HOL/ROOT Tue Aug 28 17:17:41 2012 +0200
@@ -598,20 +598,24 @@
theories [quick_and_dirty] VC_Condition
session "HOL-Ordinals_and_Cardinals-Base" in Ordinals_and_Cardinals = HOL +
+ description {* Ordinals and Cardinals, Base Theories *}
options [document = false]
theories Cardinal_Arithmetic
session "HOL-Ordinals_and_Cardinals" in Ordinals_and_Cardinals =
"HOL-Ordinals_and_Cardinals-Base" +
+ description {* Ordinals and Cardinals, Full Theories *}
options [document = pdf, document_output = "."]
theories Cardinal_Order_Relation
files "document/intro.tex" "document/root.tex" "document/root.bib"
session "HOL-Codatatype" in Codatatype = "HOL-Ordinals_and_Cardinals-Base" +
+ description {* New (Co)datatype Package *}
options [document = false]
theories Codatatype
session "HOL-Codatatype-Examples" in "Codatatype/Examples" = "HOL-Codatatype" +
+ description {* Examples for the New (Co)datatype Package *}
options [document = false]
theories
HFset
@@ -619,8 +623,7 @@
Process
TreeFsetI
(* FIXME: shouldn't require "parallel_proofs = 0";
- with parallel proofs enabled, the build of this session
- takes 10 times longer *)
+ with parallel proofs enabled, the build of this session takes 10 times longer *)
theories [parallel_proofs = 0]
"Infinite_Derivation_Trees/Gram_Lang"
"Infinite_Derivation_Trees/Parallel"