# HG changeset patch
# User blanchet
# Date 1390238696 -3600
# Node ID ef2e0fb783c6133825a4ac6222202548a47b5da7
# Parent  4e700eb471d40544bc650366857267edbbb9e9a8
tuned comments

diff -r 4e700eb471d4 -r ef2e0fb783c6 src/HOL/BNF_Cardinal_Arithmetic.thy
--- 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
diff -r 4e700eb471d4 -r ef2e0fb783c6 src/HOL/BNF_Cardinal_Order_Relation.thy
--- 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
diff -r 4e700eb471d4 -r ef2e0fb783c6 src/HOL/BNF_Comp.thy
--- 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
 
diff -r 4e700eb471d4 -r ef2e0fb783c6 src/HOL/BNF_Constructions_on_Wellorders.thy
--- 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
diff -r 4e700eb471d4 -r ef2e0fb783c6 src/HOL/BNF_Def.thy
--- 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
 
diff -r 4e700eb471d4 -r ef2e0fb783c6 src/HOL/BNF_FP_Base.thy
--- 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 *}
diff -r 4e700eb471d4 -r ef2e0fb783c6 src/HOL/BNF_GFP.thy
--- 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.
 *)
diff -r 4e700eb471d4 -r ef2e0fb783c6 src/HOL/BNF_LFP.thy
--- 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
diff -r 4e700eb471d4 -r ef2e0fb783c6 src/HOL/BNF_Util.thy
--- 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
diff -r 4e700eb471d4 -r ef2e0fb783c6 src/HOL/BNF_Wellorder_Embedding.thy
--- 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
diff -r 4e700eb471d4 -r ef2e0fb783c6 src/HOL/BNF_Wellorder_Relation.thy
--- 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