# HG changeset patch
# User blanchet
# Date 1346167061 -7200
# Node ID dcb486124b6a94839158a41b5329fbad324ff41c
# Parent  ae12b92c145a84f78670ea3fdd6230e03330ff09
tuning

diff -r ae12b92c145a -r dcb486124b6a src/HOL/ROOT
--- 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"