# HG changeset patch
# User blanchet
# Date 1348154707 -7200
# Node ID 470e612db99ab48fd990c53efe248ee1892eedb5
# Parent  e6d6869eed08e1d003fc464fa1404d3c66f085a4
the Codatatype package currently needs all of Cardinals (temporary -- because of countable sets)

diff -r e6d6869eed08 -r 470e612db99a src/HOL/ROOT
--- a/src/HOL/ROOT	Thu Sep 20 17:25:07 2012 +0200
+++ b/src/HOL/ROOT	Thu Sep 20 17:25:07 2012 +0200
@@ -610,7 +610,7 @@
     "document/root.tex"
     "document/root.bib"
 
-session "HOL-Codatatype" in Codatatype = "HOL-Cardinals-Base" +
+session "HOL-Codatatype" in Codatatype = "HOL-Cardinals" +
   description {* New (Co)datatype Package *}
   options [document = false]
   theories Codatatype