the Codatatype package currently needs all of Cardinals (temporary -- because of countable sets)
authorblanchet
Thu Sep 20 17:25:07 2012 +0200 (2012-09-20)
changeset 49483470e612db99a
parent 49482 e6d6869eed08
child 49484 0194a18f80cf
the Codatatype package currently needs all of Cardinals (temporary -- because of countable sets)
src/HOL/ROOT
     1.1 --- a/src/HOL/ROOT	Thu Sep 20 17:25:07 2012 +0200
     1.2 +++ b/src/HOL/ROOT	Thu Sep 20 17:25:07 2012 +0200
     1.3 @@ -610,7 +610,7 @@
     1.4      "document/root.tex"
     1.5      "document/root.bib"
     1.6  
     1.7 -session "HOL-Codatatype" in Codatatype = "HOL-Cardinals-Base" +
     1.8 +session "HOL-Codatatype" in Codatatype = "HOL-Cardinals" +
     1.9    description {* New (Co)datatype Package *}
    1.10    options [document = false]
    1.11    theories Codatatype