removed LICENCE note -- everything is subject to Isabelle licence as
stated in COPYRIGHT file;

--- a/src/HOLCF/Adm.thy	Wed May 25 09:04:24 2005 +0200
+++ b/src/HOLCF/Adm.thy	Wed May 25 09:44:34 2005 +0200
@@ -1,7 +1,6 @@
 (*  Title:      HOLCF/Adm.thy
     ID:         $Id$
     Author:     Franz Regensburger
-    License:    GPL (GNU GENERAL PUBLIC LICENSE)
 *)
 
 header {* Admissibility *}

--- a/src/HOLCF/Cfun.thy	Wed May 25 09:04:24 2005 +0200
+++ b/src/HOLCF/Cfun.thy	Wed May 25 09:44:34 2005 +0200
@@ -1,10 +1,8 @@
 (*  Title:      HOLCF/Cfun.thy
     ID:         $Id$
     Author:     Franz Regensburger
-    License:    GPL (GNU GENERAL PUBLIC LICENSE)
 
 Definition of the type ->  of continuous functions.
-
 *)
 
 header {* The type of continuous functions *}

--- a/src/HOLCF/Cont.thy	Wed May 25 09:04:24 2005 +0200
+++ b/src/HOLCF/Cont.thy	Wed May 25 09:44:34 2005 +0200
@@ -1,9 +1,8 @@
 (*  Title:      HOLCF/Cont.thy
     ID:         $Id$
     Author:     Franz Regensburger
-    License:    GPL (GNU GENERAL PUBLIC LICENSE)
 
-    Results about continuity and monotonicity
+Results about continuity and monotonicity.
 *)
 
 header {* Continuity and monotonicity *}

--- a/src/HOLCF/Cprod.thy	Wed May 25 09:04:24 2005 +0200
+++ b/src/HOLCF/Cprod.thy	Wed May 25 09:44:34 2005 +0200
@@ -1,9 +1,8 @@
 (*  Title:      HOLCF/Cprod.thy
     ID:         $Id$
     Author:     Franz Regensburger
-    License:    GPL (GNU GENERAL PUBLIC LICENSE)
 
-Partial ordering for cartesian product of HOL theory prod.thy
+Partial ordering for cartesian product of HOL products.
 *)
 
 header {* The cpo of cartesian products *}

--- a/src/HOLCF/Discrete.thy	Wed May 25 09:04:24 2005 +0200
+++ b/src/HOLCF/Discrete.thy	Wed May 25 09:44:34 2005 +0200
@@ -1,7 +1,6 @@
 (*  Title:      HOLCF/Discrete.thy
     ID:         $Id$
     Author:     Tobias Nipkow
-    License:    GPL (GNU GENERAL PUBLIC LICENSE)
 
 Discrete CPOs.
 *)

--- a/src/HOLCF/Domain.thy	Wed May 25 09:04:24 2005 +0200
+++ b/src/HOLCF/Domain.thy	Wed May 25 09:44:34 2005 +0200
@@ -1,7 +1,6 @@
 (*  Title:      HOLCF/Domain.thy
     ID:         $Id$
     Author:     Brian Huffman
-    License:    GPL (GNU GENERAL PUBLIC LICENSE)
 *)
 
 header {* Domain package *}

--- a/src/HOLCF/Fix.thy	Wed May 25 09:04:24 2005 +0200
+++ b/src/HOLCF/Fix.thy	Wed May 25 09:44:34 2005 +0200
@@ -1,9 +1,8 @@
 (*  Title:      HOLCF/Fix.thy
     ID:         $Id$
     Author:     Franz Regensburger
-    License:    GPL (GNU GENERAL PUBLIC LICENSE)
 
-definitions for fixed point operator and admissibility
+Definitions for fixed point operator and admissibility.
 *)
 
 header {* Fixed point operator and admissibility *}

--- a/src/HOLCF/FunCpo.thy	Wed May 25 09:04:24 2005 +0200
+++ b/src/HOLCF/FunCpo.thy	Wed May 25 09:44:34 2005 +0200
@@ -1,13 +1,12 @@
 (*  Title:      HOLCF/FunCpo.thy
     ID:         $Id$
     Author:     Franz Regensburger
-    License:    GPL (GNU GENERAL PUBLIC LICENSE)
 
 Definition of the partial ordering for the type of all functions => (fun)
 
 REMARK: The ordering on 'a => 'b is only defined if 'b is in class po !!
 
-Class instance of  => (fun) for class pcpo
+Class instance of  => (fun) for class pcpo.
 *)
 
 header {* Class instances for the type of all functions *}

--- a/src/HOLCF/One.thy	Wed May 25 09:04:24 2005 +0200
+++ b/src/HOLCF/One.thy	Wed May 25 09:44:34 2005 +0200
@@ -1,7 +1,8 @@
 (*  Title:      HOLCF/One.thy
     ID:         $Id$
     Author:     Oscar Slotosch
-    License:    GPL (GNU GENERAL PUBLIC LICENSE)
+
+The unit domain.
 *)
 
 header {* The unit domain *}
@@ -19,14 +20,6 @@
 translations
   "one" <= (type) "unit lift" 
 
-(*  Title:      HOLCF/One.ML
-    ID:         $Id$
-    Author:     Oscar Slotosch
-    License:    GPL (GNU GENERAL PUBLIC LICENSE)
-
-The unit domain.
-*)
-
 (* ------------------------------------------------------------------------ *)
 (* Exhaustion and Elimination for type one                                  *)
 (* ------------------------------------------------------------------------ *)

--- a/src/HOLCF/Pcpo.thy	Wed May 25 09:04:24 2005 +0200
+++ b/src/HOLCF/Pcpo.thy	Wed May 25 09:44:34 2005 +0200
@@ -1,9 +1,8 @@
 (*  Title:      HOLCF/Pcpo.thy
     ID:         $Id$
     Author:     Franz Regensburger
-    License:    GPL (GNU GENERAL PUBLIC LICENSE)
 
-introduction of the classes cpo and pcpo 
+Introduction of the classes cpo and pcpo.
 *)
 
 header {* Classes cpo and pcpo *}

--- a/src/HOLCF/Porder.thy	Wed May 25 09:04:24 2005 +0200
+++ b/src/HOLCF/Porder.thy	Wed May 25 09:44:34 2005 +0200
@@ -1,10 +1,9 @@
 (*  Title:      HOLCF/Porder.thy
     ID:         $Id$
     Author:     Franz Regensburger
-    License:    GPL (GNU GENERAL PUBLIC LICENSE)
 
 Definition of class porder (partial order).
-Conservative extension of theory Porder0 by constant definitions 
+Conservative extension of theory Porder0 by constant definitions.
 *)
 
 header {* Partial orders *}

--- a/src/HOLCF/Sprod.thy	Wed May 25 09:04:24 2005 +0200
+++ b/src/HOLCF/Sprod.thy	Wed May 25 09:44:34 2005 +0200
@@ -1,7 +1,6 @@
 (*  Title:      HOLCF/Sprod.thy
     ID:         $Id$
     Author:     Franz Regensburger and Brian Huffman
-    License:    GPL (GNU GENERAL PUBLIC LICENSE)
 
 Strict product with typedef.
 *)

--- a/src/HOLCF/Ssum.thy	Wed May 25 09:04:24 2005 +0200
+++ b/src/HOLCF/Ssum.thy	Wed May 25 09:44:34 2005 +0200
@@ -1,9 +1,8 @@
 (*  Title:      HOLCF/Ssum.thy
     ID:         $Id$
     Author:     Franz Regensburger and Brian Huffman
-    License:    GPL (GNU GENERAL PUBLIC LICENSE)
 
-Strict sum with typedef
+Strict sum with typedef.
 *)
 
 header {* The type of strict sums *}

--- a/src/HOLCF/Tr.thy	Wed May 25 09:04:24 2005 +0200
+++ b/src/HOLCF/Tr.thy	Wed May 25 09:44:34 2005 +0200
@@ -1,9 +1,8 @@
 (*  Title:      HOLCF/Tr.thy
     ID:         $Id$
     Author:     Franz Regensburger
-    License:    GPL (GNU GENERAL PUBLIC LICENSE)
 
-Introduce infix if_then_else_fi and boolean connectives andalso, orelse
+Introduce infix if_then_else_fi and boolean connectives andalso, orelse.
 *)
 
 header {* The type of lifted booleans *}

--- a/src/HOLCF/TypedefPcpo.thy	Wed May 25 09:04:24 2005 +0200
+++ b/src/HOLCF/TypedefPcpo.thy	Wed May 25 09:44:34 2005 +0200
@@ -1,7 +1,6 @@
 (*  Title:      HOLCF/TypedefPcpo.thy
     ID:         $Id$
     Author:     Brian Huffman
-    License:    GPL (GNU GENERAL PUBLIC LICENSE)
 *)
 
 header {* Subtypes of pcpos *}

--- a/src/HOLCF/Up.thy	Wed May 25 09:04:24 2005 +0200
+++ b/src/HOLCF/Up.thy	Wed May 25 09:44:34 2005 +0200
@@ -1,8 +1,6 @@
 (*  Title:      HOLCF/Up.thy
     ID:         $Id$
-    Author:     Franz Regensburger
-                Additions by Brian Huffman
-    License:    GPL (GNU GENERAL PUBLIC LICENSE)
+    Author:     Franz Regensburger and Brian Huffman
 
 Lifting.
 *)

--- a/src/HOLCF/domain/extender.ML	Wed May 25 09:04:24 2005 +0200
+++ b/src/HOLCF/domain/extender.ML	Wed May 25 09:44:34 2005 +0200
@@ -1,7 +1,6 @@
 (*  Title:      HOLCF/domain/extender.ML
     ID:         $Id$
     Author:     David von Oheimb
-    License:    GPL (GNU GENERAL PUBLIC LICENSE)
 
 Theory extender for domain section, including new-style theory syntax.