# HG changeset patch
# User blanchet
# Date 1390238696 -3600
# Node ID 8dd21c4b0501e1c185f52dc037003d653962a5d3
# Parent  6207fd64519bdf3d6a77ac095bdcd319ec28da43
killed obsolete session

diff -r 6207fd64519b -r 8dd21c4b0501 src/HOL/ROOT
--- 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.
   *}