--- a/src/HOL/BNF_Cardinal_Arithmetic.thy Mon Jan 20 18:24:56 2014 +0100
+++ b/src/HOL/BNF_Cardinal_Arithmetic.thy Mon Jan 20 18:24:56 2014 +0100
@@ -2,10 +2,10 @@
Author: Dmitriy Traytel, TU Muenchen
Copyright 2012
-Cardinal arithmetic (BNF).
+Cardinal arithmetic as needed by bounded natural functors.
*)
-header {* Cardinal Arithmetic (BNF) *}
+header {* Cardinal Arithmetic as Needed by Bounded Natural Functors *}
theory BNF_Cardinal_Arithmetic
imports BNF_Cardinal_Order_Relation
--- a/src/HOL/BNF_Cardinal_Order_Relation.thy Mon Jan 20 18:24:56 2014 +0100
+++ b/src/HOL/BNF_Cardinal_Order_Relation.thy Mon Jan 20 18:24:56 2014 +0100
@@ -2,10 +2,10 @@
Author: Andrei Popescu, TU Muenchen
Copyright 2012
-Cardinal-order relations (BNF).
+Cardinal-order relations as needed by bounded natural functors.
*)
-header {* Cardinal-Order Relations (BNF) *}
+header {* Cardinal-Order Relations as Needed by Bounded Natural Functors *}
theory BNF_Cardinal_Order_Relation
imports BNF_Constructions_on_Wellorders
--- a/src/HOL/BNF_Comp.thy Mon Jan 20 18:24:56 2014 +0100
+++ b/src/HOL/BNF_Comp.thy Mon Jan 20 18:24:56 2014 +0100
@@ -1,4 +1,4 @@
-(* Title: HOL/BNF/BNF_Comp.thy
+(* Title: HOL/BNF_Comp.thy
Author: Dmitriy Traytel, TU Muenchen
Copyright 2012
--- a/src/HOL/BNF_Constructions_on_Wellorders.thy Mon Jan 20 18:24:56 2014 +0100
+++ b/src/HOL/BNF_Constructions_on_Wellorders.thy Mon Jan 20 18:24:56 2014 +0100
@@ -2,10 +2,10 @@
Author: Andrei Popescu, TU Muenchen
Copyright 2012
-Constructions on wellorders (BNF).
+Constructions on wellorders as needed by bounded natural functors.
*)
-header {* Constructions on Wellorders (BNF) *}
+header {* Constructions on Wellorders as Needed by Bounded Natural Functors *}
theory BNF_Constructions_on_Wellorders
imports BNF_Wellorder_Embedding
--- a/src/HOL/BNF_Def.thy Mon Jan 20 18:24:56 2014 +0100
+++ b/src/HOL/BNF_Def.thy Mon Jan 20 18:24:56 2014 +0100
@@ -1,4 +1,4 @@
-(* Title: HOL/BNF/BNF_Def.thy
+(* Title: HOL/BNF_Def.thy
Author: Dmitriy Traytel, TU Muenchen
Copyright 2012
--- a/src/HOL/BNF_FP_Base.thy Mon Jan 20 18:24:56 2014 +0100
+++ b/src/HOL/BNF_FP_Base.thy Mon Jan 20 18:24:56 2014 +0100
@@ -1,10 +1,10 @@
-(* Title: HOL/BNF/BNF_FP_Base.thy
+(* Title: HOL/BNF_FP_Base.thy
Author: Lorenz Panny, TU Muenchen
Author: Dmitriy Traytel, TU Muenchen
Author: Jasmin Blanchette, TU Muenchen
Copyright 2012, 2013
-Shared fixed point operations on bounded natural functors, including
+Shared fixed point operations on bounded natural functors.
*)
header {* Shared Fixed Point Operations on Bounded Natural Functors *}
--- a/src/HOL/BNF_GFP.thy Mon Jan 20 18:24:56 2014 +0100
+++ b/src/HOL/BNF_GFP.thy Mon Jan 20 18:24:56 2014 +0100
@@ -1,6 +1,8 @@
-(* Title: HOL/BNF/BNF_GFP.thy
+(* Title: HOL/BNF_GFP.thy
Author: Dmitriy Traytel, TU Muenchen
- Copyright 2012
+ Author: Lorenz Panny, TU Muenchen
+ Author: Jasmin Blanchette, TU Muenchen
+ Copyright 2012, 2013
Greatest fixed point operation on bounded natural functors.
*)
--- a/src/HOL/BNF_LFP.thy Mon Jan 20 18:24:56 2014 +0100
+++ b/src/HOL/BNF_LFP.thy Mon Jan 20 18:24:56 2014 +0100
@@ -1,4 +1,4 @@
-(* Title: HOL/BNF/BNF_LFP.thy
+(* Title: HOL/BNF_LFP.thy
Author: Dmitriy Traytel, TU Muenchen
Author: Lorenz Panny, TU Muenchen
Author: Jasmin Blanchette, TU Muenchen
--- a/src/HOL/BNF_Util.thy Mon Jan 20 18:24:56 2014 +0100
+++ b/src/HOL/BNF_Util.thy Mon Jan 20 18:24:56 2014 +0100
@@ -1,4 +1,4 @@
-(* Title: HOL/BNF/BNF_Util.thy
+(* Title: HOL/BNF_Util.thy
Author: Dmitriy Traytel, TU Muenchen
Author: Jasmin Blanchette, TU Muenchen
Copyright 2012
--- a/src/HOL/BNF_Wellorder_Embedding.thy Mon Jan 20 18:24:56 2014 +0100
+++ b/src/HOL/BNF_Wellorder_Embedding.thy Mon Jan 20 18:24:56 2014 +0100
@@ -2,10 +2,10 @@
Author: Andrei Popescu, TU Muenchen
Copyright 2012
-Well-order embeddings (BNF).
+Well-order embeddings as needed by bounded natural functors.
*)
-header {* Well-Order Embeddings (BNF) *}
+header {* Well-Order Embeddings as Needed by Bounded Natural Functors *}
theory BNF_Wellorder_Embedding
imports Zorn BNF_Wellorder_Relation
--- a/src/HOL/BNF_Wellorder_Relation.thy Mon Jan 20 18:24:56 2014 +0100
+++ b/src/HOL/BNF_Wellorder_Relation.thy Mon Jan 20 18:24:56 2014 +0100
@@ -2,10 +2,10 @@
Author: Andrei Popescu, TU Muenchen
Copyright 2012
-Well-order relations (BNF).
+Well-order relations as needed by bounded natural functors.
*)
-header {* Well-Order Relations (BNF) *}
+header {* Well-Order Relations as Needed by Bounded Natural Functors *}
theory BNF_Wellorder_Relation
imports Order_Relation