use headers consistently
authorhuffman
Sun Mar 14 19:48:33 2010 -0700 (2010-03-14)
changeset 357948cd7134275cc
parent 35793 950d098c4a12
child 35795 5b95a36c1543
child 35796 2d44d2a1f68e
child 35802 362431732b5e
use headers consistently
src/HOLCF/Cfun.thy
src/HOLCF/Cont.thy
src/HOLCF/Deflation.thy
src/HOLCF/Eventual.thy
src/HOLCF/Fix.thy
src/HOLCF/Tools/Domain/domain_extender.ML
src/HOLCF/Universal.thy
     1.1 --- a/src/HOLCF/Cfun.thy	Sun Mar 14 19:47:13 2010 -0700
     1.2 +++ b/src/HOLCF/Cfun.thy	Sun Mar 14 19:48:33 2010 -0700
     1.3 @@ -1,7 +1,6 @@
     1.4  (*  Title:      HOLCF/Cfun.thy
     1.5      Author:     Franz Regensburger
     1.6 -
     1.7 -Definition of the type ->  of continuous functions.
     1.8 +    Author:     Brian Huffman
     1.9  *)
    1.10  
    1.11  header {* The type of continuous functions *}
     2.1 --- a/src/HOLCF/Cont.thy	Sun Mar 14 19:47:13 2010 -0700
     2.2 +++ b/src/HOLCF/Cont.thy	Sun Mar 14 19:48:33 2010 -0700
     2.3 @@ -1,5 +1,6 @@
     2.4  (*  Title:      HOLCF/Cont.thy
     2.5      Author:     Franz Regensburger
     2.6 +    Author:     Brian Huffman
     2.7  *)
     2.8  
     2.9  header {* Continuity and monotonicity *}
     3.1 --- a/src/HOLCF/Deflation.thy	Sun Mar 14 19:47:13 2010 -0700
     3.2 +++ b/src/HOLCF/Deflation.thy	Sun Mar 14 19:48:33 2010 -0700
     3.3 @@ -2,7 +2,7 @@
     3.4      Author:     Brian Huffman
     3.5  *)
     3.6  
     3.7 -header {* Continuous Deflations and Embedding-Projection Pairs *}
     3.8 +header {* Continuous deflations and embedding-projection pairs *}
     3.9  
    3.10  theory Deflation
    3.11  imports Cfun
     4.1 --- a/src/HOLCF/Eventual.thy	Sun Mar 14 19:47:13 2010 -0700
     4.2 +++ b/src/HOLCF/Eventual.thy	Sun Mar 14 19:48:33 2010 -0700
     4.3 @@ -1,3 +1,9 @@
     4.4 +(*  Title:      HOLCF/Eventual.thy
     4.5 +    Author:     Brian Huffman
     4.6 +*)
     4.7 +
     4.8 +header {* Eventually-constant sequences *}
     4.9 +
    4.10  theory Eventual
    4.11  imports Infinite_Set
    4.12  begin
     5.1 --- a/src/HOLCF/Fix.thy	Sun Mar 14 19:47:13 2010 -0700
     5.2 +++ b/src/HOLCF/Fix.thy	Sun Mar 14 19:48:33 2010 -0700
     5.3 @@ -1,5 +1,6 @@
     5.4  (*  Title:      HOLCF/Fix.thy
     5.5      Author:     Franz Regensburger
     5.6 +    Author:     Brian Huffman
     5.7  *)
     5.8  
     5.9  header {* Fixed point operator and admissibility *}
     6.1 --- a/src/HOLCF/Tools/Domain/domain_extender.ML	Sun Mar 14 19:47:13 2010 -0700
     6.2 +++ b/src/HOLCF/Tools/Domain/domain_extender.ML	Sun Mar 14 19:48:33 2010 -0700
     6.3 @@ -1,5 +1,6 @@
     6.4  (*  Title:      HOLCF/Tools/Domain/domain_extender.ML
     6.5      Author:     David von Oheimb
     6.6 +    Author:     Brian Huffman
     6.7  
     6.8  Theory extender for domain command, including theory syntax.
     6.9  *)
     7.1 --- a/src/HOLCF/Universal.thy	Sun Mar 14 19:47:13 2010 -0700
     7.2 +++ b/src/HOLCF/Universal.thy	Sun Mar 14 19:48:33 2010 -0700
     7.3 @@ -2,6 +2,8 @@
     7.4      Author:     Brian Huffman
     7.5  *)
     7.6  
     7.7 +header {* A universal bifinite domain *}
     7.8 +
     7.9  theory Universal
    7.10  imports CompactBasis Nat_Bijection
    7.11  begin