src/HOL/ROOT
changeset 48978 dcb486124b6a
parent 48976 2d17c305f4bc
child 48984 f51d4a302962
     1.1 --- a/src/HOL/ROOT	Tue Aug 28 17:17:25 2012 +0200
     1.2 +++ b/src/HOL/ROOT	Tue Aug 28 17:17:41 2012 +0200
     1.3 @@ -598,20 +598,24 @@
     1.4    theories [quick_and_dirty] VC_Condition
     1.5  
     1.6  session "HOL-Ordinals_and_Cardinals-Base" in Ordinals_and_Cardinals = HOL +
     1.7 +  description {* Ordinals and Cardinals, Base Theories *}
     1.8    options [document = false]
     1.9    theories Cardinal_Arithmetic
    1.10  
    1.11  session "HOL-Ordinals_and_Cardinals" in Ordinals_and_Cardinals =
    1.12      "HOL-Ordinals_and_Cardinals-Base" +
    1.13 +  description {* Ordinals and Cardinals, Full Theories *}
    1.14    options [document = pdf, document_output = "."]
    1.15    theories Cardinal_Order_Relation
    1.16    files "document/intro.tex" "document/root.tex" "document/root.bib"
    1.17  
    1.18  session "HOL-Codatatype" in Codatatype = "HOL-Ordinals_and_Cardinals-Base" +
    1.19 +  description {* New (Co)datatype Package *}
    1.20    options [document = false]
    1.21    theories Codatatype
    1.22  
    1.23  session "HOL-Codatatype-Examples" in "Codatatype/Examples" = "HOL-Codatatype" +
    1.24 +  description {* Examples for the New (Co)datatype Package *}
    1.25    options [document = false]
    1.26    theories
    1.27      HFset
    1.28 @@ -619,8 +623,7 @@
    1.29      Process
    1.30      TreeFsetI
    1.31    (* FIXME: shouldn't require "parallel_proofs = 0";
    1.32 -  with parallel proofs enabled, the build of this session
    1.33 -  takes 10 times longer *)
    1.34 +     with parallel proofs enabled, the build of this session takes 10 times longer *)
    1.35    theories [parallel_proofs = 0]
    1.36      "Infinite_Derivation_Trees/Gram_Lang"
    1.37      "Infinite_Derivation_Trees/Parallel"