src/HOL/ROOT
changeset 55064 8dd21c4b0501
parent 55054 e1f3714bc508
child 55071 8ae6f86a3477
--- a/src/HOL/ROOT	Mon Jan 20 18:24:56 2014 +0100
+++ b/src/HOL/ROOT	Mon Jan 20 18:24:56 2014 +0100
@@ -699,14 +699,7 @@
     "document/root.tex"
     "document/root.bib"
 
-session "HOL-BNF-FP" in BNF = HOL +
-  description {*
-    Bounded Natural Functors for (Co)datatypes, Fixpoints.
-  *}
-  options [document = false]
-  theories BNF_LFP BNF_GFP
-
-session "HOL-BNF" in BNF = "HOL-BNF-FP" +
+session "HOL-BNF" in BNF = HOL +
   description {*
     Bounded Natural Functors for (Co)datatypes, Including More BNFs.
   *}