# HG changeset patch
# User blanchet
# Date 1348239218 -7200
# Node ID 9f5bfef8bd8265cd3fa2024220e0349c97f636d4
# Parent  ba50d204095ee87b266bc907da9172f3e5c35af5
created separate session "HOL-BNF-LFP" as a step towards eventual integration in "HOL" in the middle term

diff -r ba50d204095e -r 9f5bfef8bd82 src/HOL/ROOT
--- a/src/HOL/ROOT	Fri Sep 21 16:45:06 2012 +0200
+++ b/src/HOL/ROOT	Fri Sep 21 16:53:38 2012 +0200
@@ -604,13 +604,19 @@
 
 session "HOL-Cardinals" in Cardinals = "HOL-Cardinals-Base" +
   description {* Ordinals and Cardinals, Full Theories *}
+  options [document = false]
   theories Cardinals
   files
     "document/intro.tex"
     "document/root.tex"
     "document/root.bib"
 
-session "HOL-BNF" in BNF = "HOL-Cardinals" +
+session "HOL-BNF-LFP" in BNF = "HOL-Cardinals-Base" +
+  description {* Bounded Natural Functors for Datatypes *}
+  options [document = false]
+  theories BNF_LFP
+
+session "HOL-BNF" in BNF = "HOL-BNF-LFP" +
   description {* Bounded Natural Functors for (Co)datatypes *}
   options [document = false]
   theories BNF