--- /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
--- 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
--- 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
--- 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
--- 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
--- 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
--- 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
--- 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
--- 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
--- 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
--- 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
--- 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
--- 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
--- 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
--- 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
--- 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]
--- 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
--- 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
--- 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"
--- 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
--- 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
--- 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
--- 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
--- 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
--- 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
--- 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
--- 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>)—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>
--- 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
--- 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
--- 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
--- 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
--- 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
--- 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
--- 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
--- 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
--- 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
--- 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
--- 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
--- 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
--- 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
--- 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
--- 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
--- 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
--- 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