--- a/src/HOL/ROOT Tue Aug 28 16:33:06 2012 +0200
+++ b/src/HOL/ROOT Tue Aug 28 17:16:00 2012 +0200
@@ -597,6 +597,37 @@
theories Nominal_Examples
theories [quick_and_dirty] VC_Condition
+session "HOL-Ordinals_and_Cardinals-Base" in Ordinals_and_Cardinals = HOL +
+ options [document = false]
+ theories Cardinal_Arithmetic
+
+session "HOL-Ordinals_and_Cardinals" in Ordinals_and_Cardinals =
+ "HOL-Ordinals_and_Cardinals-Base" +
+ options [document = false]
+ theories Cardinal_Order_Relation
+
+session "HOL-Codatatype" in Codatatype = "HOL-Ordinals_and_Cardinals-Base" +
+ options [document = false]
+ theories Codatatype
+
+session "HOL-Codatatype-Examples" in "Codatatype/Examples" = "HOL-Codatatype" +
+ options [document = false]
+ theories
+ HFset
+ Lambda_Term
+ Process
+ TreeFsetI
+ (* FIXME: shouldn't require "parallel_proofs = 0";
+ 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"
+ Stream
+ theories [parallel_proofs = 0, condition = ISABELLE_FULL_TEST]
+ Misc_Codata
+ Misc_Data
+
session "HOL-Word" in Word = HOL +
options [document_graph]
theories Word