1.1 --- a/src/HOL/ROOT	Mon Nov 18 18:04:44 2013 +0100
     1.2 +++ b/src/HOL/ROOT	Mon Nov 18 18:04:44 2013 +0100
     1.3 @@ -687,14 +687,14 @@
     1.4    theories Nominal_Examples
     1.5    theories [quick_and_dirty] VC_Condition
     1.6  
     1.7 -session "HOL-Cardinals-Base" in Cardinals = HOL +
     1.8 +session "HOL-Cardinals-LFP" in Cardinals = HOL +
     1.9    description {*
    1.10 -    Ordinals and Cardinals, Base Theories.
    1.11 +    Ordinals and Cardinals, Theories Needed for BNF LFP Construction.
    1.12    *}
    1.13    options [document = false]
    1.14    theories Cardinal_Arithmetic
    1.15  
    1.16 -session "HOL-Cardinals" in Cardinals = "HOL-Cardinals-Base" +
    1.17 +session "HOL-Cardinals" in Cardinals = "HOL-Cardinals-LFP" +
    1.18    description {*
    1.19      Ordinals and Cardinals, Full Theories.
    1.20    *}
    1.21 @@ -705,7 +705,7 @@
    1.22      "document/root.tex"
    1.23      "document/root.bib"
    1.24  
    1.25 -session "HOL-BNF-LFP" in BNF = "HOL-Cardinals-Base" +
    1.26 +session "HOL-BNF-LFP" in BNF = "HOL-Cardinals-LFP" +
    1.27    description {*
    1.28      Bounded Natural Functors for Datatypes.
    1.29    *}