src/HOL/ROOT
changeset 49310 6e30078de4f0
parent 49110 2e43fb45b91b
child 49349 be27a453aacc
     1.1 --- a/src/HOL/ROOT	Wed Sep 12 05:21:47 2012 +0200
     1.2 +++ b/src/HOL/ROOT	Wed Sep 12 05:29:21 2012 +0200
     1.3 @@ -597,13 +597,12 @@
     1.4    theories Nominal_Examples
     1.5    theories [quick_and_dirty] VC_Condition
     1.6  
     1.7 -session "HOL-Ordinals_and_Cardinals-Base" in Ordinals_and_Cardinals = HOL +
     1.8 +session "HOL-Cardinals-Base" in Cardinals = HOL +
     1.9    description {* Ordinals and Cardinals, Base Theories *}
    1.10    options [document = false]
    1.11    theories Cardinal_Arithmetic
    1.12  
    1.13 -session "HOL-Ordinals_and_Cardinals" in Ordinals_and_Cardinals =
    1.14 -    "HOL-Ordinals_and_Cardinals-Base" +
    1.15 +session "HOL-Cardinals" in Cardinals = "HOL-Cardinals-Base" +
    1.16    description {* Ordinals and Cardinals, Full Theories *}
    1.17    theories Cardinal_Order_Relation
    1.18    files
    1.19 @@ -611,7 +610,7 @@
    1.20      "document/root.tex"
    1.21      "document/root.bib"
    1.22  
    1.23 -session "HOL-Codatatype" in Codatatype = "HOL-Ordinals_and_Cardinals-Base" +
    1.24 +session "HOL-Codatatype" in Codatatype = "HOL-Cardinals-Base" +
    1.25    description {* New (Co)datatype Package *}
    1.26    options [document = false]
    1.27    theories Codatatype