tuned comments
authorblanchet
Mon Jan 20 18:24:56 2014 +0100 (2014-01-20)
changeset 55059ef2e0fb783c6
parent 55058 4e700eb471d4
child 55060 3105434fb02f
tuned comments
src/HOL/BNF_Cardinal_Arithmetic.thy
src/HOL/BNF_Cardinal_Order_Relation.thy
src/HOL/BNF_Comp.thy
src/HOL/BNF_Constructions_on_Wellorders.thy
src/HOL/BNF_Def.thy
src/HOL/BNF_FP_Base.thy
src/HOL/BNF_GFP.thy
src/HOL/BNF_LFP.thy
src/HOL/BNF_Util.thy
src/HOL/BNF_Wellorder_Embedding.thy
src/HOL/BNF_Wellorder_Relation.thy
     1.1 --- a/src/HOL/BNF_Cardinal_Arithmetic.thy	Mon Jan 20 18:24:56 2014 +0100
     1.2 +++ b/src/HOL/BNF_Cardinal_Arithmetic.thy	Mon Jan 20 18:24:56 2014 +0100
     1.3 @@ -2,10 +2,10 @@
     1.4      Author:     Dmitriy Traytel, TU Muenchen
     1.5      Copyright   2012
     1.6  
     1.7 -Cardinal arithmetic (BNF).
     1.8 +Cardinal arithmetic as needed by bounded natural functors.
     1.9  *)
    1.10  
    1.11 -header {* Cardinal Arithmetic (BNF) *}
    1.12 +header {* Cardinal Arithmetic as Needed by Bounded Natural Functors *}
    1.13  
    1.14  theory BNF_Cardinal_Arithmetic
    1.15  imports BNF_Cardinal_Order_Relation
     2.1 --- a/src/HOL/BNF_Cardinal_Order_Relation.thy	Mon Jan 20 18:24:56 2014 +0100
     2.2 +++ b/src/HOL/BNF_Cardinal_Order_Relation.thy	Mon Jan 20 18:24:56 2014 +0100
     2.3 @@ -2,10 +2,10 @@
     2.4      Author:     Andrei Popescu, TU Muenchen
     2.5      Copyright   2012
     2.6  
     2.7 -Cardinal-order relations (BNF).
     2.8 +Cardinal-order relations as needed by bounded natural functors.
     2.9  *)
    2.10  
    2.11 -header {* Cardinal-Order Relations (BNF) *}
    2.12 +header {* Cardinal-Order Relations as Needed by Bounded Natural Functors *}
    2.13  
    2.14  theory BNF_Cardinal_Order_Relation
    2.15  imports BNF_Constructions_on_Wellorders
     3.1 --- a/src/HOL/BNF_Comp.thy	Mon Jan 20 18:24:56 2014 +0100
     3.2 +++ b/src/HOL/BNF_Comp.thy	Mon Jan 20 18:24:56 2014 +0100
     3.3 @@ -1,4 +1,4 @@
     3.4 -(*  Title:      HOL/BNF/BNF_Comp.thy
     3.5 +(*  Title:      HOL/BNF_Comp.thy
     3.6      Author:     Dmitriy Traytel, TU Muenchen
     3.7      Copyright   2012
     3.8  
     4.1 --- a/src/HOL/BNF_Constructions_on_Wellorders.thy	Mon Jan 20 18:24:56 2014 +0100
     4.2 +++ b/src/HOL/BNF_Constructions_on_Wellorders.thy	Mon Jan 20 18:24:56 2014 +0100
     4.3 @@ -2,10 +2,10 @@
     4.4      Author:     Andrei Popescu, TU Muenchen
     4.5      Copyright   2012
     4.6  
     4.7 -Constructions on wellorders (BNF).
     4.8 +Constructions on wellorders as needed by bounded natural functors.
     4.9  *)
    4.10  
    4.11 -header {* Constructions on Wellorders (BNF) *}
    4.12 +header {* Constructions on Wellorders as Needed by Bounded Natural Functors *}
    4.13  
    4.14  theory BNF_Constructions_on_Wellorders
    4.15  imports BNF_Wellorder_Embedding
     5.1 --- a/src/HOL/BNF_Def.thy	Mon Jan 20 18:24:56 2014 +0100
     5.2 +++ b/src/HOL/BNF_Def.thy	Mon Jan 20 18:24:56 2014 +0100
     5.3 @@ -1,4 +1,4 @@
     5.4 -(*  Title:      HOL/BNF/BNF_Def.thy
     5.5 +(*  Title:      HOL/BNF_Def.thy
     5.6      Author:     Dmitriy Traytel, TU Muenchen
     5.7      Copyright   2012
     5.8  
     6.1 --- a/src/HOL/BNF_FP_Base.thy	Mon Jan 20 18:24:56 2014 +0100
     6.2 +++ b/src/HOL/BNF_FP_Base.thy	Mon Jan 20 18:24:56 2014 +0100
     6.3 @@ -1,10 +1,10 @@
     6.4 -(*  Title:      HOL/BNF/BNF_FP_Base.thy
     6.5 +(*  Title:      HOL/BNF_FP_Base.thy
     6.6      Author:     Lorenz Panny, TU Muenchen
     6.7      Author:     Dmitriy Traytel, TU Muenchen
     6.8      Author:     Jasmin Blanchette, TU Muenchen
     6.9      Copyright   2012, 2013
    6.10  
    6.11 -Shared fixed point operations on bounded natural functors, including
    6.12 +Shared fixed point operations on bounded natural functors.
    6.13  *)
    6.14  
    6.15  header {* Shared Fixed Point Operations on Bounded Natural Functors *}
     7.1 --- a/src/HOL/BNF_GFP.thy	Mon Jan 20 18:24:56 2014 +0100
     7.2 +++ b/src/HOL/BNF_GFP.thy	Mon Jan 20 18:24:56 2014 +0100
     7.3 @@ -1,6 +1,8 @@
     7.4 -(*  Title:      HOL/BNF/BNF_GFP.thy
     7.5 +(*  Title:      HOL/BNF_GFP.thy
     7.6      Author:     Dmitriy Traytel, TU Muenchen
     7.7 -    Copyright   2012
     7.8 +    Author:     Lorenz Panny, TU Muenchen
     7.9 +    Author:     Jasmin Blanchette, TU Muenchen
    7.10 +    Copyright   2012, 2013
    7.11  
    7.12  Greatest fixed point operation on bounded natural functors.
    7.13  *)
     8.1 --- a/src/HOL/BNF_LFP.thy	Mon Jan 20 18:24:56 2014 +0100
     8.2 +++ b/src/HOL/BNF_LFP.thy	Mon Jan 20 18:24:56 2014 +0100
     8.3 @@ -1,4 +1,4 @@
     8.4 -(*  Title:      HOL/BNF/BNF_LFP.thy
     8.5 +(*  Title:      HOL/BNF_LFP.thy
     8.6      Author:     Dmitriy Traytel, TU Muenchen
     8.7      Author:     Lorenz Panny, TU Muenchen
     8.8      Author:     Jasmin Blanchette, TU Muenchen
     9.1 --- a/src/HOL/BNF_Util.thy	Mon Jan 20 18:24:56 2014 +0100
     9.2 +++ b/src/HOL/BNF_Util.thy	Mon Jan 20 18:24:56 2014 +0100
     9.3 @@ -1,4 +1,4 @@
     9.4 -(*  Title:      HOL/BNF/BNF_Util.thy
     9.5 +(*  Title:      HOL/BNF_Util.thy
     9.6      Author:     Dmitriy Traytel, TU Muenchen
     9.7      Author:     Jasmin Blanchette, TU Muenchen
     9.8      Copyright   2012
    10.1 --- a/src/HOL/BNF_Wellorder_Embedding.thy	Mon Jan 20 18:24:56 2014 +0100
    10.2 +++ b/src/HOL/BNF_Wellorder_Embedding.thy	Mon Jan 20 18:24:56 2014 +0100
    10.3 @@ -2,10 +2,10 @@
    10.4      Author:     Andrei Popescu, TU Muenchen
    10.5      Copyright   2012
    10.6  
    10.7 -Well-order embeddings (BNF).
    10.8 +Well-order embeddings as needed by bounded natural functors.
    10.9  *)
   10.10  
   10.11 -header {* Well-Order Embeddings (BNF) *}
   10.12 +header {* Well-Order Embeddings as Needed by Bounded Natural Functors *}
   10.13  
   10.14  theory BNF_Wellorder_Embedding
   10.15  imports Zorn BNF_Wellorder_Relation
    11.1 --- a/src/HOL/BNF_Wellorder_Relation.thy	Mon Jan 20 18:24:56 2014 +0100
    11.2 +++ b/src/HOL/BNF_Wellorder_Relation.thy	Mon Jan 20 18:24:56 2014 +0100
    11.3 @@ -2,10 +2,10 @@
    11.4      Author:     Andrei Popescu, TU Muenchen
    11.5      Copyright   2012
    11.6  
    11.7 -Well-order relations (BNF).
    11.8 +Well-order relations as needed by bounded natural functors.
    11.9  *)
   11.10  
   11.11 -header {* Well-Order Relations (BNF) *}
   11.12 +header {* Well-Order Relations as Needed by Bounded Natural Functors *}
   11.13  
   11.14  theory BNF_Wellorder_Relation
   11.15  imports Order_Relation