# HG changeset patch
# User blanchet
# Date 1348238080 -7200
# Node ID 163914705f8d2e8be0776630ef8183e43817c8e1
# Parent  1e205327f0592f6fcd5f071240fa6b979cfd7979
renamed top-level theory from "Codatatype" to "BNF"

diff -r 1e205327f059 -r 163914705f8d src/HOL/Codatatype/BNF.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Codatatype/BNF.thy	Fri Sep 21 16:34:40 2012 +0200
@@ -0,0 +1,16 @@
+(*  Title:      HOL/BNF/BNF.thy
+    Author:     Dmitriy Traytel, TU Muenchen
+    Author:     Andrei Popescu, TU Muenchen
+    Author:     Jasmin Blanchette, TU Muenchen
+    Copyright   2012
+
+Bounded natural functors for (co)datatypes.
+*)
+
+header {* Bounded Natural Functors for (Co)datatypes *}
+
+theory BNF
+imports More_BNFs
+begin
+
+end
diff -r 1e205327f059 -r 163914705f8d src/HOL/Codatatype/BNF_Comp.thy
--- a/src/HOL/Codatatype/BNF_Comp.thy	Fri Sep 21 15:53:29 2012 +0200
+++ b/src/HOL/Codatatype/BNF_Comp.thy	Fri Sep 21 16:34:40 2012 +0200
@@ -1,4 +1,4 @@
-(*  Title:      HOL/Codatatype/BNF_Comp.thy
+(*  Title:      HOL/BNF/BNF_Comp.thy
     Author:     Dmitriy Traytel, TU Muenchen
     Copyright   2012
 
diff -r 1e205327f059 -r 163914705f8d src/HOL/Codatatype/BNF_Def.thy
--- a/src/HOL/Codatatype/BNF_Def.thy	Fri Sep 21 15:53:29 2012 +0200
+++ b/src/HOL/Codatatype/BNF_Def.thy	Fri Sep 21 16:34:40 2012 +0200
@@ -1,4 +1,4 @@
-(*  Title:      HOL/Codatatype/BNF_Def.thy
+(*  Title:      HOL/BNF/BNF_Def.thy
     Author:     Dmitriy Traytel, TU Muenchen
     Copyright   2012
 
diff -r 1e205327f059 -r 163914705f8d src/HOL/Codatatype/BNF_FP.thy
--- a/src/HOL/Codatatype/BNF_FP.thy	Fri Sep 21 15:53:29 2012 +0200
+++ b/src/HOL/Codatatype/BNF_FP.thy	Fri Sep 21 16:34:40 2012 +0200
@@ -1,4 +1,4 @@
-(*  Title:      HOL/Codatatype/BNF_FP.thy
+(*  Title:      HOL/BNF/BNF_FP.thy
     Author:     Dmitriy Traytel, TU Muenchen
     Author:     Jasmin Blanchette, TU Muenchen
     Copyright   2012
diff -r 1e205327f059 -r 163914705f8d src/HOL/Codatatype/BNF_GFP.thy
--- a/src/HOL/Codatatype/BNF_GFP.thy	Fri Sep 21 15:53:29 2012 +0200
+++ b/src/HOL/Codatatype/BNF_GFP.thy	Fri Sep 21 16:34:40 2012 +0200
@@ -1,4 +1,4 @@
-(*  Title:      HOL/Codatatype/BNF_GFP.thy
+(*  Title:      HOL/BNF/BNF_GFP.thy
     Author:     Dmitriy Traytel, TU Muenchen
     Copyright   2012
 
diff -r 1e205327f059 -r 163914705f8d src/HOL/Codatatype/BNF_LFP.thy
--- a/src/HOL/Codatatype/BNF_LFP.thy	Fri Sep 21 15:53:29 2012 +0200
+++ b/src/HOL/Codatatype/BNF_LFP.thy	Fri Sep 21 16:34:40 2012 +0200
@@ -1,4 +1,4 @@
-(*  Title:      HOL/Codatatype/BNF_LFP.thy
+(*  Title:      HOL/BNF/BNF_LFP.thy
     Author:     Dmitriy Traytel, TU Muenchen
     Copyright   2012
 
diff -r 1e205327f059 -r 163914705f8d src/HOL/Codatatype/BNF_Util.thy
--- a/src/HOL/Codatatype/BNF_Util.thy	Fri Sep 21 15:53:29 2012 +0200
+++ b/src/HOL/Codatatype/BNF_Util.thy	Fri Sep 21 16:34:40 2012 +0200
@@ -1,4 +1,4 @@
-(*  Title:      HOL/Codatatype/BNF_Util.thy
+(*  Title:      HOL/BNF/BNF_Util.thy
     Author:     Dmitriy Traytel, TU Muenchen
     Author:     Jasmin Blanchette, TU Muenchen
     Copyright   2012
diff -r 1e205327f059 -r 163914705f8d src/HOL/Codatatype/BNF_Wrap.thy
--- a/src/HOL/Codatatype/BNF_Wrap.thy	Fri Sep 21 15:53:29 2012 +0200
+++ b/src/HOL/Codatatype/BNF_Wrap.thy	Fri Sep 21 16:34:40 2012 +0200
@@ -1,4 +1,4 @@
-(*  Title:      HOL/Codatatype/BNF_Wrap.thy
+(*  Title:      HOL/BNF/BNF_Wrap.thy
     Author:     Jasmin Blanchette, TU Muenchen
     Copyright   2012
 
diff -r 1e205327f059 -r 163914705f8d src/HOL/Codatatype/Basic_BNFs.thy
--- a/src/HOL/Codatatype/Basic_BNFs.thy	Fri Sep 21 15:53:29 2012 +0200
+++ b/src/HOL/Codatatype/Basic_BNFs.thy	Fri Sep 21 16:34:40 2012 +0200
@@ -1,4 +1,4 @@
-(*  Title:      HOL/Codatatype/Basic_BNFs.thy
+(*  Title:      HOL/BNF/Basic_BNFs.thy
     Author:     Dmitriy Traytel, TU Muenchen
     Author:     Andrei Popescu, TU Muenchen
     Author:     Jasmin Blanchette, TU Muenchen
diff -r 1e205327f059 -r 163914705f8d src/HOL/Codatatype/Codatatype.thy
--- a/src/HOL/Codatatype/Codatatype.thy	Fri Sep 21 15:53:29 2012 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,16 +0,0 @@
-(*  Title:      HOL/Codatatype/Codatatype.thy
-    Author:     Dmitriy Traytel, TU Muenchen
-    Author:     Andrei Popescu, TU Muenchen
-    Author:     Jasmin Blanchette, TU Muenchen
-    Copyright   2012
-
-The (co)datatype package.
-*)
-
-header {* The (Co)datatype Package *}
-
-theory Codatatype
-imports More_BNFs
-begin
-
-end
diff -r 1e205327f059 -r 163914705f8d src/HOL/Codatatype/Countable_Set.thy
--- a/src/HOL/Codatatype/Countable_Set.thy	Fri Sep 21 15:53:29 2012 +0200
+++ b/src/HOL/Codatatype/Countable_Set.thy	Fri Sep 21 16:34:40 2012 +0200
@@ -1,4 +1,4 @@
-(*  Title:      HOL/Codatatype/Countable_Set.thy
+(*  Title:      HOL/BNF/Countable_Set.thy
     Author:     Andrei Popescu, TU Muenchen
     Copyright   2012
 
diff -r 1e205327f059 -r 163914705f8d src/HOL/Codatatype/Equiv_Relations_More.thy
--- a/src/HOL/Codatatype/Equiv_Relations_More.thy	Fri Sep 21 15:53:29 2012 +0200
+++ b/src/HOL/Codatatype/Equiv_Relations_More.thy	Fri Sep 21 16:34:40 2012 +0200
@@ -1,4 +1,4 @@
-(*  Title:      HOL/Codatatype/Equiv_Relations_More.thy
+(*  Title:      HOL/BNF/Equiv_Relations_More.thy
     Author:     Andrei Popescu, TU Muenchen
     Copyright   2012
 
diff -r 1e205327f059 -r 163914705f8d src/HOL/Codatatype/Examples/HFset.thy
--- a/src/HOL/Codatatype/Examples/HFset.thy	Fri Sep 21 15:53:29 2012 +0200
+++ b/src/HOL/Codatatype/Examples/HFset.thy	Fri Sep 21 16:34:40 2012 +0200
@@ -1,4 +1,4 @@
-(*  Title:      HOL/Codatatype/Examples/HFset.thy
+(*  Title:      HOL/BNF/Examples/HFset.thy
     Author:     Andrei Popescu, TU Muenchen
     Copyright   2012
 
@@ -8,7 +8,7 @@
 header {* Hereditary Sets *}
 
 theory HFset
-imports "../Codatatype"
+imports "../BNF"
 begin
 
 
diff -r 1e205327f059 -r 163914705f8d src/HOL/Codatatype/Examples/Infinite_Derivation_Trees/Gram_Lang.thy
--- a/src/HOL/Codatatype/Examples/Infinite_Derivation_Trees/Gram_Lang.thy	Fri Sep 21 15:53:29 2012 +0200
+++ b/src/HOL/Codatatype/Examples/Infinite_Derivation_Trees/Gram_Lang.thy	Fri Sep 21 16:34:40 2012 +0200
@@ -1,4 +1,4 @@
-(*  Title:      HOL/Codatatype/Examples/Infinite_Derivation_Trees/Gram_Lang.thy
+(*  Title:      HOL/BNF/Examples/Infinite_Derivation_Trees/Gram_Lang.thy
     Author:     Andrei Popescu, TU Muenchen
     Copyright   2012
 
diff -r 1e205327f059 -r 163914705f8d src/HOL/Codatatype/Examples/Infinite_Derivation_Trees/Parallel.thy
--- a/src/HOL/Codatatype/Examples/Infinite_Derivation_Trees/Parallel.thy	Fri Sep 21 15:53:29 2012 +0200
+++ b/src/HOL/Codatatype/Examples/Infinite_Derivation_Trees/Parallel.thy	Fri Sep 21 16:34:40 2012 +0200
@@ -1,4 +1,4 @@
-(*  Title:      HOL/Codatatype/Examples/Infinite_Derivation_Trees/Parallel.thy
+(*  Title:      HOL/BNF/Examples/Infinite_Derivation_Trees/Parallel.thy
     Author:     Andrei Popescu, TU Muenchen
     Copyright   2012
 
diff -r 1e205327f059 -r 163914705f8d src/HOL/Codatatype/Examples/Infinite_Derivation_Trees/Prelim.thy
--- a/src/HOL/Codatatype/Examples/Infinite_Derivation_Trees/Prelim.thy	Fri Sep 21 15:53:29 2012 +0200
+++ b/src/HOL/Codatatype/Examples/Infinite_Derivation_Trees/Prelim.thy	Fri Sep 21 16:34:40 2012 +0200
@@ -1,4 +1,4 @@
-(*  Title:      HOL/Codatatype/Examples/Infinite_Derivation_Trees/Prelim.thy
+(*  Title:      HOL/BNF/Examples/Infinite_Derivation_Trees/Prelim.thy
     Author:     Andrei Popescu, TU Muenchen
     Copyright   2012
 
@@ -8,7 +8,7 @@
 header {* Preliminaries *}
 
 theory Prelim
-imports "../../Codatatype/Codatatype"
+imports "../../BNF"
 begin
 
 declare fset_to_fset[simp]
diff -r 1e205327f059 -r 163914705f8d src/HOL/Codatatype/Examples/Infinite_Derivation_Trees/Tree.thy
--- a/src/HOL/Codatatype/Examples/Infinite_Derivation_Trees/Tree.thy	Fri Sep 21 15:53:29 2012 +0200
+++ b/src/HOL/Codatatype/Examples/Infinite_Derivation_Trees/Tree.thy	Fri Sep 21 16:34:40 2012 +0200
@@ -1,4 +1,4 @@
-(*  Title:      HOL/Codatatype/Examples/Infinite_Derivation_Trees/Tree.thy
+(*  Title:      HOL/BNF/Examples/Infinite_Derivation_Trees/Tree.thy
     Author:     Andrei Popescu, TU Muenchen
     Copyright   2012
 
diff -r 1e205327f059 -r 163914705f8d src/HOL/Codatatype/Examples/Lambda_Term.thy
--- a/src/HOL/Codatatype/Examples/Lambda_Term.thy	Fri Sep 21 15:53:29 2012 +0200
+++ b/src/HOL/Codatatype/Examples/Lambda_Term.thy	Fri Sep 21 16:34:40 2012 +0200
@@ -1,4 +1,4 @@
-(*  Title:      HOL/Codatatype/Examples/Lambda_Term.thy
+(*  Title:      HOL/BNF/Examples/Lambda_Term.thy
     Author:     Dmitriy Traytel, TU Muenchen
     Author:     Andrei Popescu, TU Muenchen
     Copyright   2012
@@ -9,7 +9,7 @@
 header {* Lambda-Terms *}
 
 theory Lambda_Term
-imports "../Codatatype"
+imports "../BNF"
 begin
 
 
diff -r 1e205327f059 -r 163914705f8d src/HOL/Codatatype/Examples/ListF.thy
--- a/src/HOL/Codatatype/Examples/ListF.thy	Fri Sep 21 15:53:29 2012 +0200
+++ b/src/HOL/Codatatype/Examples/ListF.thy	Fri Sep 21 16:34:40 2012 +0200
@@ -1,4 +1,4 @@
-(*  Title:      HOL/Codatatype/Examples/ListF.thy
+(*  Title:      HOL/BNF/Examples/ListF.thy
     Author:     Dmitriy Traytel, TU Muenchen
     Author:     Andrei Popescu, TU Muenchen
     Copyright   2012
@@ -9,7 +9,7 @@
 header {* Finite Lists *}
 
 theory ListF
-imports "../Codatatype"
+imports "../BNF"
 begin
 
 data_raw listF: 'list = "unit + 'a \<times> 'list"
diff -r 1e205327f059 -r 163914705f8d src/HOL/Codatatype/Examples/Misc_Codata.thy
--- a/src/HOL/Codatatype/Examples/Misc_Codata.thy	Fri Sep 21 15:53:29 2012 +0200
+++ b/src/HOL/Codatatype/Examples/Misc_Codata.thy	Fri Sep 21 16:34:40 2012 +0200
@@ -1,4 +1,4 @@
-(*  Title:      HOL/Codatatype/Examples/Misc_Data.thy
+(*  Title:      HOL/BNF/Examples/Misc_Data.thy
     Author:     Dmitriy Traytel, TU Muenchen
     Author:     Andrei Popescu, TU Muenchen
     Copyright   2012
@@ -9,7 +9,7 @@
 header {* Miscellaneous Codatatype Declarations *}
 
 theory Misc_Codata
-imports "../Codatatype"
+imports "../BNF"
 begin
 
 codata simple = X1 | X2 | X3 | X4
diff -r 1e205327f059 -r 163914705f8d src/HOL/Codatatype/Examples/Misc_Data.thy
--- a/src/HOL/Codatatype/Examples/Misc_Data.thy	Fri Sep 21 15:53:29 2012 +0200
+++ b/src/HOL/Codatatype/Examples/Misc_Data.thy	Fri Sep 21 16:34:40 2012 +0200
@@ -1,4 +1,4 @@
-(*  Title:      HOL/Codatatype/Examples/Misc_Data.thy
+(*  Title:      HOL/BNF/Examples/Misc_Data.thy
     Author:     Dmitriy Traytel, TU Muenchen
     Author:     Andrei Popescu, TU Muenchen
     Copyright   2012
@@ -9,7 +9,7 @@
 header {* Miscellaneous Datatype Declarations *}
 
 theory Misc_Data
-imports "../Codatatype"
+imports "../BNF"
 begin
 
 data simple = X1 | X2 | X3 | X4
diff -r 1e205327f059 -r 163914705f8d src/HOL/Codatatype/Examples/Process.thy
--- a/src/HOL/Codatatype/Examples/Process.thy	Fri Sep 21 15:53:29 2012 +0200
+++ b/src/HOL/Codatatype/Examples/Process.thy	Fri Sep 21 16:34:40 2012 +0200
@@ -1,4 +1,4 @@
-(*  Title:      HOL/Codatatype/Examples/Process.thy
+(*  Title:      HOL/BNF/Examples/Process.thy
     Author:     Andrei Popescu, TU Muenchen
     Copyright   2012
 
@@ -8,7 +8,7 @@
 header {* Processes *}
 
 theory Process
-imports "../Codatatype"
+imports "../BNF"
 begin
 
 hide_fact (open) Quotient_Product.prod_rel_def
diff -r 1e205327f059 -r 163914705f8d src/HOL/Codatatype/Examples/Stream.thy
--- a/src/HOL/Codatatype/Examples/Stream.thy	Fri Sep 21 15:53:29 2012 +0200
+++ b/src/HOL/Codatatype/Examples/Stream.thy	Fri Sep 21 16:34:40 2012 +0200
@@ -1,4 +1,4 @@
-(*  Title:      HOL/Codatatype/Examples/Stream.thy
+(*  Title:      HOL/BNF/Examples/Stream.thy
     Author:     Dmitriy Traytel, TU Muenchen
     Author:     Andrei Popescu, TU Muenchen
     Copyright   2012
diff -r 1e205327f059 -r 163914705f8d src/HOL/Codatatype/Examples/TreeFI.thy
--- a/src/HOL/Codatatype/Examples/TreeFI.thy	Fri Sep 21 15:53:29 2012 +0200
+++ b/src/HOL/Codatatype/Examples/TreeFI.thy	Fri Sep 21 16:34:40 2012 +0200
@@ -1,4 +1,4 @@
-(*  Title:      HOL/Codatatype/Examples/TreeFI.thy
+(*  Title:      HOL/BNF/Examples/TreeFI.thy
     Author:     Dmitriy Traytel, TU Muenchen
     Author:     Andrei Popescu, TU Muenchen
     Copyright   2012
diff -r 1e205327f059 -r 163914705f8d src/HOL/Codatatype/Examples/TreeFsetI.thy
--- a/src/HOL/Codatatype/Examples/TreeFsetI.thy	Fri Sep 21 15:53:29 2012 +0200
+++ b/src/HOL/Codatatype/Examples/TreeFsetI.thy	Fri Sep 21 16:34:40 2012 +0200
@@ -1,4 +1,4 @@
-(*  Title:      HOL/Codatatype/Examples/TreeFsetI.thy
+(*  Title:      HOL/BNF/Examples/TreeFsetI.thy
     Author:     Dmitriy Traytel, TU Muenchen
     Author:     Andrei Popescu, TU Muenchen
     Copyright   2012
@@ -9,7 +9,7 @@
 header {* Finitely Branching Possibly Infinite Trees, with Sets of Children *}
 
 theory TreeFsetI
-imports "../Codatatype"
+imports "../BNF"
 begin
 
 hide_const (open) Sublist.sub
diff -r 1e205327f059 -r 163914705f8d src/HOL/Codatatype/More_BNFs.thy
--- a/src/HOL/Codatatype/More_BNFs.thy	Fri Sep 21 15:53:29 2012 +0200
+++ b/src/HOL/Codatatype/More_BNFs.thy	Fri Sep 21 16:34:40 2012 +0200
@@ -1,4 +1,4 @@
-(*  Title:      HOL/Codatatype/More_BNFs.thy
+(*  Title:      HOL/BNF/More_BNFs.thy
     Author:     Dmitriy Traytel, TU Muenchen
     Author:     Andrei Popescu, TU Muenchen
     Author:     Andreas Lochbihler, Karlsruhe Institute of Technology
diff -r 1e205327f059 -r 163914705f8d src/HOL/Codatatype/README.html
--- a/src/HOL/Codatatype/README.html	Fri Sep 21 15:53:29 2012 +0200
+++ b/src/HOL/Codatatype/README.html	Fri Sep 21 16:34:40 2012 +0200
@@ -4,21 +4,20 @@
 
 <head>
   <meta http-equiv="Content-Type" content="text/html; charset=iso-8859-1">
-  <title>Codatatype Package</title>
+  <title>BNF Package</title>
 </head>
 
 <body>
 
-<h3><i>Codatatype</i>: A (co)datatype package based on bounded natural functors
+<h3><i>BNF</i>: A (co)datatype package based on bounded natural functors
 (BNFs)</h3>
 
 <p>
-The <i>Codatatype</i> package provides a fully modular framework for
-constructing inductive and coinductive datatypes in HOL, with support for mixed
-mutual and nested (co)recursion. Mixed (co)recursion enables type definitions
-involving both datatypes and codatatypes, such as the type of finitely branching
-trees of possibly infinite depth. The framework draws heavily from category
-theory.
+The <i>BNF</i> package provides a fully modular framework for constructing
+inductive and coinductive datatypes in HOL, with support for mixed mutual and
+nested (co)recursion. Mixed (co)recursion enables type definitions involving
+both datatypes and codatatypes, such as the type of finitely branching trees of
+possibly infinite depth. The framework draws heavily from category theory.
 
 <p>
 The package is described in the following paper:
@@ -30,24 +29,21 @@
 </ul>
 
 <p>
-The main entry point for applications is <tt>Codatatype.thy</tt>.
-The <tt>Examples</tt> directory contains various examples of (co)datatypes,
-including the examples from the paper.
+The main entry point for applications is <tt>BNF.thy</tt>. The <tt>Examples</tt>
+directory contains various examples of (co)datatypes, including the examples
+from the paper.
 
 <p>
 The key notion underlying the package is that of a <i>bounded natural functor</i>
 (<i>BNF</i>)&mdash;an enriched type constructor satisfying specific properties
 preserved by interesting categorical operations (composition, least fixed point,
-and greatest fixed point). The <tt>Basic_BNFs.thy</tt> file registers
-various basic types, notably for sums, products, function spaces, finite sets,
-multisets, and countable sets. Custom BNFs can be registered as well.
+and greatest fixed point). The <tt>Basic_BNFs.thy</tt> and <tt>More_BNFs.thy</tt>
+files register various basic types, notably for sums, products, function spaces,
+finite sets, multisets, and countable sets. Custom BNFs can be registered as well.
 
 <p>
-<b>Warning:</b> The package is under development. Future versions are expected
-to support multiple constructors and selectors per (co)datatype (instead of a
-single <i>fld</i> or <i>unf</i> constant) and provide a nicer syntax for
-(co)induction and (co)recursive function definitions. Please contact
-any nonempty subset of
+<b>Warning:</b> The package is under development. Please contact any nonempty
+subset of
 <a href="mailto:traytel@in.tum.de">the</a>
 <a href="mailto:popescua@in.tum.de">above</a>
 <a href="mailto:blanchette@in.tum.de">authors</a>
diff -r 1e205327f059 -r 163914705f8d src/HOL/Codatatype/Tools/bnf_comp.ML
--- a/src/HOL/Codatatype/Tools/bnf_comp.ML	Fri Sep 21 15:53:29 2012 +0200
+++ b/src/HOL/Codatatype/Tools/bnf_comp.ML	Fri Sep 21 16:34:40 2012 +0200
@@ -1,4 +1,4 @@
-(*  Title:      HOL/Codatatype/Tools/bnf_comp.ML
+(*  Title:      HOL/BNF/Tools/bnf_comp.ML
     Author:     Dmitriy Traytel, TU Muenchen
     Author:     Jasmin Blanchette, TU Muenchen
     Copyright   2012
diff -r 1e205327f059 -r 163914705f8d src/HOL/Codatatype/Tools/bnf_comp_tactics.ML
--- a/src/HOL/Codatatype/Tools/bnf_comp_tactics.ML	Fri Sep 21 15:53:29 2012 +0200
+++ b/src/HOL/Codatatype/Tools/bnf_comp_tactics.ML	Fri Sep 21 16:34:40 2012 +0200
@@ -1,4 +1,4 @@
-(*  Title:      HOL/Codatatype/Tools/bnf_comp_tactics.ML
+(*  Title:      HOL/BNF/Tools/bnf_comp_tactics.ML
     Author:     Dmitriy Traytel, TU Muenchen
     Author:     Jasmin Blanchette, TU Muenchen
     Copyright   2012
diff -r 1e205327f059 -r 163914705f8d src/HOL/Codatatype/Tools/bnf_def.ML
--- a/src/HOL/Codatatype/Tools/bnf_def.ML	Fri Sep 21 15:53:29 2012 +0200
+++ b/src/HOL/Codatatype/Tools/bnf_def.ML	Fri Sep 21 16:34:40 2012 +0200
@@ -1,4 +1,4 @@
-(*  Title:      HOL/Codatatype/Tools/bnf_def.ML
+(*  Title:      HOL/BNF/Tools/bnf_def.ML
     Author:     Dmitriy Traytel, TU Muenchen
     Author:     Jasmin Blanchette, TU Muenchen
     Copyright   2012
diff -r 1e205327f059 -r 163914705f8d src/HOL/Codatatype/Tools/bnf_def_tactics.ML
--- a/src/HOL/Codatatype/Tools/bnf_def_tactics.ML	Fri Sep 21 15:53:29 2012 +0200
+++ b/src/HOL/Codatatype/Tools/bnf_def_tactics.ML	Fri Sep 21 16:34:40 2012 +0200
@@ -1,4 +1,4 @@
-(*  Title:      HOL/Codatatype/Tools/bnf_def_tactics.ML
+(*  Title:      HOL/BNF/Tools/bnf_def_tactics.ML
     Author:     Dmitriy Traytel, TU Muenchen
     Author:     Jasmin Blanchette, TU Muenchen
     Copyright   2012
diff -r 1e205327f059 -r 163914705f8d src/HOL/Codatatype/Tools/bnf_fp.ML
--- a/src/HOL/Codatatype/Tools/bnf_fp.ML	Fri Sep 21 15:53:29 2012 +0200
+++ b/src/HOL/Codatatype/Tools/bnf_fp.ML	Fri Sep 21 16:34:40 2012 +0200
@@ -1,4 +1,4 @@
-(*  Title:      HOL/Codatatype/Tools/bnf_fp.ML
+(*  Title:      HOL/BNF/Tools/bnf_fp.ML
     Author:     Dmitriy Traytel, TU Muenchen
     Copyright   2012
 
diff -r 1e205327f059 -r 163914705f8d src/HOL/Codatatype/Tools/bnf_fp_sugar.ML
--- a/src/HOL/Codatatype/Tools/bnf_fp_sugar.ML	Fri Sep 21 15:53:29 2012 +0200
+++ b/src/HOL/Codatatype/Tools/bnf_fp_sugar.ML	Fri Sep 21 16:34:40 2012 +0200
@@ -1,4 +1,4 @@
-(*  Title:      HOL/Codatatype/Tools/bnf_fp_sugar.ML
+(*  Title:      HOL/BNF/Tools/bnf_fp_sugar.ML
     Author:     Jasmin Blanchette, TU Muenchen
     Copyright   2012
 
diff -r 1e205327f059 -r 163914705f8d src/HOL/Codatatype/Tools/bnf_fp_sugar_tactics.ML
--- a/src/HOL/Codatatype/Tools/bnf_fp_sugar_tactics.ML	Fri Sep 21 15:53:29 2012 +0200
+++ b/src/HOL/Codatatype/Tools/bnf_fp_sugar_tactics.ML	Fri Sep 21 16:34:40 2012 +0200
@@ -1,4 +1,4 @@
-(*  Title:      HOL/Codatatype/Tools/bnf_fp_sugar_tactics.ML
+(*  Title:      HOL/BNF/Tools/bnf_fp_sugar_tactics.ML
     Author:     Jasmin Blanchette, TU Muenchen
     Copyright   2012
 
diff -r 1e205327f059 -r 163914705f8d src/HOL/Codatatype/Tools/bnf_gfp.ML
--- a/src/HOL/Codatatype/Tools/bnf_gfp.ML	Fri Sep 21 15:53:29 2012 +0200
+++ b/src/HOL/Codatatype/Tools/bnf_gfp.ML	Fri Sep 21 16:34:40 2012 +0200
@@ -1,4 +1,4 @@
-(*  Title:      HOL/Codatatype/Tools/bnf_gfp.ML
+(*  Title:      HOL/BNF/Tools/bnf_gfp.ML
     Author:     Dmitriy Traytel, TU Muenchen
     Author:     Andrei Popescu, TU Muenchen
     Author:     Jasmin Blanchette, TU Muenchen
diff -r 1e205327f059 -r 163914705f8d src/HOL/Codatatype/Tools/bnf_gfp_tactics.ML
--- a/src/HOL/Codatatype/Tools/bnf_gfp_tactics.ML	Fri Sep 21 15:53:29 2012 +0200
+++ b/src/HOL/Codatatype/Tools/bnf_gfp_tactics.ML	Fri Sep 21 16:34:40 2012 +0200
@@ -1,4 +1,4 @@
-(*  Title:      HOL/Codatatype/Tools/bnf_gfp_tactics.ML
+(*  Title:      HOL/BNF/Tools/bnf_gfp_tactics.ML
     Author:     Dmitriy Traytel, TU Muenchen
     Author:     Andrei Popescu, TU Muenchen
     Author:     Jasmin Blanchette, TU Muenchen
diff -r 1e205327f059 -r 163914705f8d src/HOL/Codatatype/Tools/bnf_gfp_util.ML
--- a/src/HOL/Codatatype/Tools/bnf_gfp_util.ML	Fri Sep 21 15:53:29 2012 +0200
+++ b/src/HOL/Codatatype/Tools/bnf_gfp_util.ML	Fri Sep 21 16:34:40 2012 +0200
@@ -1,4 +1,4 @@
-(*  Title:      HOL/Codatatype/Tools/bnf_gfp_util.ML
+(*  Title:      HOL/BNF/Tools/bnf_gfp_util.ML
     Author:     Dmitriy Traytel, TU Muenchen
     Copyright   2012
 
diff -r 1e205327f059 -r 163914705f8d src/HOL/Codatatype/Tools/bnf_lfp.ML
--- a/src/HOL/Codatatype/Tools/bnf_lfp.ML	Fri Sep 21 15:53:29 2012 +0200
+++ b/src/HOL/Codatatype/Tools/bnf_lfp.ML	Fri Sep 21 16:34:40 2012 +0200
@@ -1,4 +1,4 @@
-(*  Title:      HOL/Codatatype/Tools/bnf_lfp.ML
+(*  Title:      HOL/BNF/Tools/bnf_lfp.ML
     Author:     Dmitriy Traytel, TU Muenchen
     Author:     Andrei Popescu, TU Muenchen
     Copyright   2012
diff -r 1e205327f059 -r 163914705f8d src/HOL/Codatatype/Tools/bnf_lfp_tactics.ML
--- a/src/HOL/Codatatype/Tools/bnf_lfp_tactics.ML	Fri Sep 21 15:53:29 2012 +0200
+++ b/src/HOL/Codatatype/Tools/bnf_lfp_tactics.ML	Fri Sep 21 16:34:40 2012 +0200
@@ -1,4 +1,4 @@
-(*  Title:      HOL/Codatatype/Tools/bnf_lfp_tactics.ML
+(*  Title:      HOL/BNF/Tools/bnf_lfp_tactics.ML
     Author:     Dmitriy Traytel, TU Muenchen
     Author:     Andrei Popescu, TU Muenchen
     Copyright   2012
diff -r 1e205327f059 -r 163914705f8d src/HOL/Codatatype/Tools/bnf_lfp_util.ML
--- a/src/HOL/Codatatype/Tools/bnf_lfp_util.ML	Fri Sep 21 15:53:29 2012 +0200
+++ b/src/HOL/Codatatype/Tools/bnf_lfp_util.ML	Fri Sep 21 16:34:40 2012 +0200
@@ -1,4 +1,4 @@
-(*  Title:      Codatatype_Tools/bnf_lfp_util.ML
+(*  Title:      HOL/BNF/Tools/bnf_lfp_util.ML
     Author:     Dmitriy Traytel, TU Muenchen
     Author:     Jasmin Blanchette, TU Muenchen
     Copyright   2012
diff -r 1e205327f059 -r 163914705f8d src/HOL/Codatatype/Tools/bnf_tactics.ML
--- a/src/HOL/Codatatype/Tools/bnf_tactics.ML	Fri Sep 21 15:53:29 2012 +0200
+++ b/src/HOL/Codatatype/Tools/bnf_tactics.ML	Fri Sep 21 16:34:40 2012 +0200
@@ -1,4 +1,4 @@
-(*  Title:      HOL/Codatatype/Tools/bnf_tactics.ML
+(*  Title:      HOL/BNF/Tools/bnf_tactics.ML
     Author:     Dmitriy Traytel, TU Muenchen
     Author:     Jasmin Blanchette, TU Muenchen
     Copyright   2012
diff -r 1e205327f059 -r 163914705f8d src/HOL/Codatatype/Tools/bnf_util.ML
--- a/src/HOL/Codatatype/Tools/bnf_util.ML	Fri Sep 21 15:53:29 2012 +0200
+++ b/src/HOL/Codatatype/Tools/bnf_util.ML	Fri Sep 21 16:34:40 2012 +0200
@@ -1,4 +1,4 @@
-(*  Title:      HOL/Codatatype/Tools/bnf_util.ML
+(*  Title:      HOL/BNF/Tools/bnf_util.ML
     Author:     Dmitriy Traytel, TU Muenchen
     Copyright   2012
 
diff -r 1e205327f059 -r 163914705f8d src/HOL/Codatatype/Tools/bnf_wrap.ML
--- a/src/HOL/Codatatype/Tools/bnf_wrap.ML	Fri Sep 21 15:53:29 2012 +0200
+++ b/src/HOL/Codatatype/Tools/bnf_wrap.ML	Fri Sep 21 16:34:40 2012 +0200
@@ -1,4 +1,4 @@
-(*  Title:      HOL/Codatatype/Tools/bnf_wrap.ML
+(*  Title:      HOL/BNF/Tools/bnf_wrap.ML
     Author:     Jasmin Blanchette, TU Muenchen
     Copyright   2012
 
diff -r 1e205327f059 -r 163914705f8d src/HOL/Codatatype/Tools/bnf_wrap_tactics.ML
--- a/src/HOL/Codatatype/Tools/bnf_wrap_tactics.ML	Fri Sep 21 15:53:29 2012 +0200
+++ b/src/HOL/Codatatype/Tools/bnf_wrap_tactics.ML	Fri Sep 21 16:34:40 2012 +0200
@@ -1,4 +1,4 @@
-(*  Title:      HOL/Codatatype/Tools/bnf_wrap_tactics.ML
+(*  Title:      HOL/BNF/Tools/bnf_wrap_tactics.ML
     Author:     Jasmin Blanchette, TU Muenchen
     Copyright   2012