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. *}