# HG changeset patch
# User huffman
# Date 1268621313 25200
# Node ID 8cd7134275cc3cbfc046a5fbc1b930aa2ed726c3
# Parent  950d098c4a121d6cf8797cd9a3fa8e8541ea6434
use headers consistently

diff -r 950d098c4a12 -r 8cd7134275cc src/HOLCF/Cfun.thy
--- a/src/HOLCF/Cfun.thy	Sun Mar 14 19:47:13 2010 -0700
+++ b/src/HOLCF/Cfun.thy	Sun Mar 14 19:48:33 2010 -0700
@@ -1,7 +1,6 @@
 (*  Title:      HOLCF/Cfun.thy
     Author:     Franz Regensburger
-
-Definition of the type ->  of continuous functions.
+    Author:     Brian Huffman
 *)
 
 header {* The type of continuous functions *}
diff -r 950d098c4a12 -r 8cd7134275cc src/HOLCF/Cont.thy
--- a/src/HOLCF/Cont.thy	Sun Mar 14 19:47:13 2010 -0700
+++ b/src/HOLCF/Cont.thy	Sun Mar 14 19:48:33 2010 -0700
@@ -1,5 +1,6 @@
 (*  Title:      HOLCF/Cont.thy
     Author:     Franz Regensburger
+    Author:     Brian Huffman
 *)
 
 header {* Continuity and monotonicity *}
diff -r 950d098c4a12 -r 8cd7134275cc src/HOLCF/Deflation.thy
--- a/src/HOLCF/Deflation.thy	Sun Mar 14 19:47:13 2010 -0700
+++ b/src/HOLCF/Deflation.thy	Sun Mar 14 19:48:33 2010 -0700
@@ -2,7 +2,7 @@
     Author:     Brian Huffman
 *)
 
-header {* Continuous Deflations and Embedding-Projection Pairs *}
+header {* Continuous deflations and embedding-projection pairs *}
 
 theory Deflation
 imports Cfun
diff -r 950d098c4a12 -r 8cd7134275cc src/HOLCF/Eventual.thy
--- a/src/HOLCF/Eventual.thy	Sun Mar 14 19:47:13 2010 -0700
+++ b/src/HOLCF/Eventual.thy	Sun Mar 14 19:48:33 2010 -0700
@@ -1,3 +1,9 @@
+(*  Title:      HOLCF/Eventual.thy
+    Author:     Brian Huffman
+*)
+
+header {* Eventually-constant sequences *}
+
 theory Eventual
 imports Infinite_Set
 begin
diff -r 950d098c4a12 -r 8cd7134275cc src/HOLCF/Fix.thy
--- a/src/HOLCF/Fix.thy	Sun Mar 14 19:47:13 2010 -0700
+++ b/src/HOLCF/Fix.thy	Sun Mar 14 19:48:33 2010 -0700
@@ -1,5 +1,6 @@
 (*  Title:      HOLCF/Fix.thy
     Author:     Franz Regensburger
+    Author:     Brian Huffman
 *)
 
 header {* Fixed point operator and admissibility *}
diff -r 950d098c4a12 -r 8cd7134275cc src/HOLCF/Tools/Domain/domain_extender.ML
--- a/src/HOLCF/Tools/Domain/domain_extender.ML	Sun Mar 14 19:47:13 2010 -0700
+++ b/src/HOLCF/Tools/Domain/domain_extender.ML	Sun Mar 14 19:48:33 2010 -0700
@@ -1,5 +1,6 @@
 (*  Title:      HOLCF/Tools/Domain/domain_extender.ML
     Author:     David von Oheimb
+    Author:     Brian Huffman
 
 Theory extender for domain command, including theory syntax.
 *)
diff -r 950d098c4a12 -r 8cd7134275cc src/HOLCF/Universal.thy
--- a/src/HOLCF/Universal.thy	Sun Mar 14 19:47:13 2010 -0700
+++ b/src/HOLCF/Universal.thy	Sun Mar 14 19:48:33 2010 -0700
@@ -2,6 +2,8 @@
     Author:     Brian Huffman
 *)
 
+header {* A universal bifinite domain *}
+
 theory Universal
 imports CompactBasis Nat_Bijection
 begin