created separate session "HOL-BNF-LFP" as a step towards eventual integration in "HOL" in the middle term
authorblanchet
Fri Sep 21 16:53:38 2012 +0200 (2012-09-21)
changeset 495119f5bfef8bd82
parent 49510 ba50d204095e
child 49512 82d99fe04018
created separate session "HOL-BNF-LFP" as a step towards eventual integration in "HOL" in the middle term
src/HOL/ROOT
     1.1 --- a/src/HOL/ROOT	Fri Sep 21 16:45:06 2012 +0200
     1.2 +++ b/src/HOL/ROOT	Fri Sep 21 16:53:38 2012 +0200
     1.3 @@ -604,13 +604,19 @@
     1.4  
     1.5  session "HOL-Cardinals" in Cardinals = "HOL-Cardinals-Base" +
     1.6    description {* Ordinals and Cardinals, Full Theories *}
     1.7 +  options [document = false]
     1.8    theories Cardinals
     1.9    files
    1.10      "document/intro.tex"
    1.11      "document/root.tex"
    1.12      "document/root.bib"
    1.13  
    1.14 -session "HOL-BNF" in BNF = "HOL-Cardinals" +
    1.15 +session "HOL-BNF-LFP" in BNF = "HOL-Cardinals-Base" +
    1.16 +  description {* Bounded Natural Functors for Datatypes *}
    1.17 +  options [document = false]
    1.18 +  theories BNF_LFP
    1.19 +
    1.20 +session "HOL-BNF" in BNF = "HOL-BNF-LFP" +
    1.21    description {* Bounded Natural Functors for (Co)datatypes *}
    1.22    options [document = false]
    1.23    theories BNF