--- 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 *}
--- 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 *}
--- 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
--- 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
--- 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 *}
--- 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.
*)
--- 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