# HG changeset patch
# User wenzelm
# Date 1004748086 -3600
# Node ID 46d57d0290a24de6bda4325f039c91ceb7f7020a
# Parent  7df1d840d01dbb469774f8a286211bef12439f62
GPLed;

diff -r 7df1d840d01d -r 46d57d0290a2 src/HOLCF/Cfun1.ML
--- a/src/HOLCF/Cfun1.ML	Sat Nov 03 01:40:28 2001 +0100
+++ b/src/HOLCF/Cfun1.ML	Sat Nov 03 01:41:26 2001 +0100
@@ -1,7 +1,7 @@
 (*  Title:      HOLCF/Cfun1.ML
     ID:         $Id$
     Author:     Franz Regensburger
-    Copyright   1993 Technische Universitaet Muenchen
+    License:    GPL (GNU GENERAL PUBLIC LICENSE)
 
 The type ->  of continuous functions.
 *)
diff -r 7df1d840d01d -r 46d57d0290a2 src/HOLCF/Cfun1.thy
--- a/src/HOLCF/Cfun1.thy	Sat Nov 03 01:40:28 2001 +0100
+++ b/src/HOLCF/Cfun1.thy	Sat Nov 03 01:41:26 2001 +0100
@@ -1,7 +1,7 @@
 (*  Title:      HOLCF/Cfun1.thy
     ID:         $Id$
     Author:     Franz Regensburger
-    Copyright   1993 Technische Universitaet Muenchen
+    License:    GPL (GNU GENERAL PUBLIC LICENSE)
 
 Definition of the type ->  of continuous functions.
 
diff -r 7df1d840d01d -r 46d57d0290a2 src/HOLCF/Cfun2.ML
--- a/src/HOLCF/Cfun2.ML	Sat Nov 03 01:40:28 2001 +0100
+++ b/src/HOLCF/Cfun2.ML	Sat Nov 03 01:41:26 2001 +0100
@@ -1,7 +1,7 @@
 (*  Title:      HOLCF/Cfun2
     ID:         $Id$
     Author:     Franz Regensburger
-    Copyright   1993 Technische Universitaet Muenchen
+    License:    GPL (GNU GENERAL PUBLIC LICENSE)
 
 Class Instance ->::(cpo,cpo)po
 *)
diff -r 7df1d840d01d -r 46d57d0290a2 src/HOLCF/Cfun2.thy
--- a/src/HOLCF/Cfun2.thy	Sat Nov 03 01:40:28 2001 +0100
+++ b/src/HOLCF/Cfun2.thy	Sat Nov 03 01:41:26 2001 +0100
@@ -1,7 +1,7 @@
 (*  Title:      HOLCF/Cfun2.thy
     ID:         $Id$
     Author:     Franz Regensburger
-    Copyright   1993 Technische Universitaet Muenchen
+    License:    GPL (GNU GENERAL PUBLIC LICENSE)
 
 Class Instance ->::(cpo,cpo)po
 
diff -r 7df1d840d01d -r 46d57d0290a2 src/HOLCF/Cfun3.ML
--- a/src/HOLCF/Cfun3.ML	Sat Nov 03 01:40:28 2001 +0100
+++ b/src/HOLCF/Cfun3.ML	Sat Nov 03 01:41:26 2001 +0100
@@ -1,7 +1,7 @@
 (*  Title:      HOLCF/Cfun3
     ID:         $Id$
     Author:     Franz Regensburger
-    Copyright   1993 Technische Universitaet Muenchen
+    License:    GPL (GNU GENERAL PUBLIC LICENSE)
 
 Class instance of  -> for class pcpo
 *)
diff -r 7df1d840d01d -r 46d57d0290a2 src/HOLCF/Cfun3.thy
--- a/src/HOLCF/Cfun3.thy	Sat Nov 03 01:40:28 2001 +0100
+++ b/src/HOLCF/Cfun3.thy	Sat Nov 03 01:41:26 2001 +0100
@@ -1,7 +1,7 @@
 (*  Title:      HOLCF/Cfun3.thy
     ID:         $Id$
     Author:     Franz Regensburger
-    Copyright   1993 Technische Universitaet Muenchen
+    License:    GPL (GNU GENERAL PUBLIC LICENSE)
 
 Class instance of  -> for class pcpo
 
diff -r 7df1d840d01d -r 46d57d0290a2 src/HOLCF/Cont.ML
--- a/src/HOLCF/Cont.ML	Sat Nov 03 01:40:28 2001 +0100
+++ b/src/HOLCF/Cont.ML	Sat Nov 03 01:41:26 2001 +0100
@@ -1,7 +1,7 @@
 (*  Title:      HOLCF/Cont.ML
     ID:         $Id$
     Author:     Franz Regensburger
-    Copyright   1993 Technische Universitaet Muenchen
+    License:    GPL (GNU GENERAL PUBLIC LICENSE)
 
 Results about continuity and monotonicity
 *)
diff -r 7df1d840d01d -r 46d57d0290a2 src/HOLCF/Cont.thy
--- a/src/HOLCF/Cont.thy	Sat Nov 03 01:40:28 2001 +0100
+++ b/src/HOLCF/Cont.thy	Sat Nov 03 01:41:26 2001 +0100
@@ -1,7 +1,7 @@
 (*  Title:      HOLCF/cont.thy
     ID:         $Id$
     Author:     Franz Regensburger
-    Copyright   1993 Technische Universitaet Muenchen
+    License:    GPL (GNU GENERAL PUBLIC LICENSE)
 
     Results about continuity and monotonicity
 *)
diff -r 7df1d840d01d -r 46d57d0290a2 src/HOLCF/Cprod1.ML
--- a/src/HOLCF/Cprod1.ML	Sat Nov 03 01:40:28 2001 +0100
+++ b/src/HOLCF/Cprod1.ML	Sat Nov 03 01:41:26 2001 +0100
@@ -1,7 +1,7 @@
 (*  Title:      HOLCF/Cprod1.ML
     ID:         $Id$
     Author:     Franz Regensburger
-    Copyright   1993  Technische Universitaet Muenchen
+    License:    GPL (GNU GENERAL PUBLIC LICENSE)
 
 Partial ordering for cartesian product of HOL theory Product_Type.thy
 *)
diff -r 7df1d840d01d -r 46d57d0290a2 src/HOLCF/Cprod1.thy
--- a/src/HOLCF/Cprod1.thy	Sat Nov 03 01:40:28 2001 +0100
+++ b/src/HOLCF/Cprod1.thy	Sat Nov 03 01:41:26 2001 +0100
@@ -1,11 +1,9 @@
 (*  Title:      HOLCF/Cprod1.thy
     ID:         $Id$
     Author:     Franz Regensburger
-    Copyright   1993  Technische Universitaet Muenchen
-
+    License:    GPL (GNU GENERAL PUBLIC LICENSE)
 
 Partial ordering for cartesian product of HOL theory prod.thy
-
 *)
 
 Cprod1 = Cfun3 +
diff -r 7df1d840d01d -r 46d57d0290a2 src/HOLCF/Cprod2.ML
--- a/src/HOLCF/Cprod2.ML	Sat Nov 03 01:40:28 2001 +0100
+++ b/src/HOLCF/Cprod2.ML	Sat Nov 03 01:41:26 2001 +0100
@@ -1,7 +1,7 @@
 (*  Title:      HOLCF/Cprod2
     ID:         $Id$
     Author:     Franz Regensburger
-    Copyright   1993 Technische Universitaet Muenchen
+    License:    GPL (GNU GENERAL PUBLIC LICENSE)
 
 Class Instance *::(pcpo,pcpo)po
 *)
diff -r 7df1d840d01d -r 46d57d0290a2 src/HOLCF/Cprod2.thy
--- a/src/HOLCF/Cprod2.thy	Sat Nov 03 01:40:28 2001 +0100
+++ b/src/HOLCF/Cprod2.thy	Sat Nov 03 01:41:26 2001 +0100
@@ -1,7 +1,7 @@
 (*  Title:      HOLCF/Cprod2.thy
     ID:         $Id$
     Author:     Franz Regensburger
-    Copyright   1993 Technische Universitaet Muenchen
+    License:    GPL (GNU GENERAL PUBLIC LICENSE)
 
 Class Instance *::(pcpo,pcpo)po
 
diff -r 7df1d840d01d -r 46d57d0290a2 src/HOLCF/Cprod3.ML
--- a/src/HOLCF/Cprod3.ML	Sat Nov 03 01:40:28 2001 +0100
+++ b/src/HOLCF/Cprod3.ML	Sat Nov 03 01:41:26 2001 +0100
@@ -1,7 +1,7 @@
 (*  Title:      HOLCF/Cprod3
     ID:         $Id$
     Author:     Franz Regensburger
-    Copyright   1993 Technische Universitaet Muenchen
+    License:    GPL (GNU GENERAL PUBLIC LICENSE)
 
 Class instance of * for class pcpo and cpo.
 *)
diff -r 7df1d840d01d -r 46d57d0290a2 src/HOLCF/Cprod3.thy
--- a/src/HOLCF/Cprod3.thy	Sat Nov 03 01:40:28 2001 +0100
+++ b/src/HOLCF/Cprod3.thy	Sat Nov 03 01:41:26 2001 +0100
@@ -1,7 +1,7 @@
 (*  Title:      HOLCF/Cprod3.thy
     ID:         $Id$
     Author:     Franz Regensburger
-    Copyright   1993 Technische Universitaet Muenchen
+    License:    GPL (GNU GENERAL PUBLIC LICENSE)
 
 Class instance of * for class pcpo and cpo.
 *)
diff -r 7df1d840d01d -r 46d57d0290a2 src/HOLCF/Discrete.ML
--- a/src/HOLCF/Discrete.ML	Sat Nov 03 01:40:28 2001 +0100
+++ b/src/HOLCF/Discrete.ML	Sat Nov 03 01:41:26 2001 +0100
@@ -1,7 +1,7 @@
 (*  Title:      HOLCF/Discrete.ML
     ID:         $Id$
     Author:     Tobias Nipkow
-    Copyright   1997 TUM
+    License:    GPL (GNU GENERAL PUBLIC LICENSE)
 *)
 
 Goalw [undiscr_def] "undiscr(Discr x) = x";
diff -r 7df1d840d01d -r 46d57d0290a2 src/HOLCF/Discrete.thy
--- a/src/HOLCF/Discrete.thy	Sat Nov 03 01:40:28 2001 +0100
+++ b/src/HOLCF/Discrete.thy	Sat Nov 03 01:41:26 2001 +0100
@@ -1,9 +1,9 @@
 (*  Title:      HOLCF/Discrete.thy
     ID:         $Id$
     Author:     Tobias Nipkow
-    Copyright   1997 TUM
+    License:    GPL (GNU GENERAL PUBLIC LICENSE)
 
-Discrete CPOs
+Discrete CPOs.
 *)
 
 Discrete = Discrete1 +
diff -r 7df1d840d01d -r 46d57d0290a2 src/HOLCF/Discrete0.ML
--- a/src/HOLCF/Discrete0.ML	Sat Nov 03 01:40:28 2001 +0100
+++ b/src/HOLCF/Discrete0.ML	Sat Nov 03 01:41:26 2001 +0100
@@ -1,7 +1,7 @@
 (*  Title:      HOLCF/Discrete0.ML
     ID:         $Id$
     Author:     Tobias Nipkow
-    Copyright   1997 TUM
+    License:    GPL (GNU GENERAL PUBLIC LICENSE)
 
 Proves that 'a discr is a po
 *)
diff -r 7df1d840d01d -r 46d57d0290a2 src/HOLCF/Discrete0.thy
--- a/src/HOLCF/Discrete0.thy	Sat Nov 03 01:40:28 2001 +0100
+++ b/src/HOLCF/Discrete0.thy	Sat Nov 03 01:41:26 2001 +0100
@@ -1,9 +1,9 @@
 (*  Title:      HOLCF/Discrete0.thy
     ID:         $Id$
     Author:     Tobias Nipkow
-    Copyright   1997 TUM
+    License:    GPL (GNU GENERAL PUBLIC LICENSE)
 
-Discrete CPOs
+Discrete CPOs.
 *)
 
 Discrete0 = Cont + Datatype +
diff -r 7df1d840d01d -r 46d57d0290a2 src/HOLCF/Discrete1.ML
--- a/src/HOLCF/Discrete1.ML	Sat Nov 03 01:40:28 2001 +0100
+++ b/src/HOLCF/Discrete1.ML	Sat Nov 03 01:41:26 2001 +0100
@@ -1,7 +1,7 @@
 (*  Title:      HOLCF/Discrete1.ML
     ID:         $Id$
     Author:     Tobias Nipkow
-    Copyright   1997 TUM
+    License:    GPL (GNU GENERAL PUBLIC LICENSE)
 
 Proves that 'a discr is a cpo
 *)
diff -r 7df1d840d01d -r 46d57d0290a2 src/HOLCF/Discrete1.thy
--- a/src/HOLCF/Discrete1.thy	Sat Nov 03 01:40:28 2001 +0100
+++ b/src/HOLCF/Discrete1.thy	Sat Nov 03 01:41:26 2001 +0100
@@ -1,9 +1,9 @@
 (*  Title:      HOLCF/Discrete1.thy
     ID:         $Id$
     Author:     Tobias Nipkow
-    Copyright   1997 TUM
+    License:    GPL (GNU GENERAL PUBLIC LICENSE)
 
-Discrete CPOs
+Discrete CPOs.
 *)
 
 Discrete1 = Discrete0 +
diff -r 7df1d840d01d -r 46d57d0290a2 src/HOLCF/Fix.ML
--- a/src/HOLCF/Fix.ML	Sat Nov 03 01:40:28 2001 +0100
+++ b/src/HOLCF/Fix.ML	Sat Nov 03 01:41:26 2001 +0100
@@ -1,7 +1,7 @@
 (*  Title:      HOLCF/Fix.ML
     ID:         $Id$
     Author:     Franz Regensburger
-    Copyright   1993  Technische Universitaet Muenchen
+    License:    GPL (GNU GENERAL PUBLIC LICENSE)
 
 fixed point operator and admissibility
 *)
diff -r 7df1d840d01d -r 46d57d0290a2 src/HOLCF/Fix.thy
--- a/src/HOLCF/Fix.thy	Sat Nov 03 01:40:28 2001 +0100
+++ b/src/HOLCF/Fix.thy	Sat Nov 03 01:41:26 2001 +0100
@@ -1,11 +1,9 @@
 (*  Title:      HOLCF/Fix.thy
     ID:         $Id$
     Author:     Franz Regensburger
-    Copyright   1993  Technische Universitaet Muenchen
-
+    License:    GPL (GNU GENERAL PUBLIC LICENSE)
 
 definitions for fixed point operator and admissibility
-
 *)
 
 Fix = Cfun3 +
diff -r 7df1d840d01d -r 46d57d0290a2 src/HOLCF/Fun1.ML
--- a/src/HOLCF/Fun1.ML	Sat Nov 03 01:40:28 2001 +0100
+++ b/src/HOLCF/Fun1.ML	Sat Nov 03 01:41:26 2001 +0100
@@ -1,7 +1,7 @@
 (*  Title:      HOLCF/Fun1.ML
     ID:         $Id$
     Author:     Franz Regensburger
-    Copyright   1993  Technische Universitaet Muenchen
+    License:    GPL (GNU GENERAL PUBLIC LICENSE)
 
 Definition of the partial ordering for the type of all functions => (fun)
 *)
diff -r 7df1d840d01d -r 46d57d0290a2 src/HOLCF/Fun1.thy
--- a/src/HOLCF/Fun1.thy	Sat Nov 03 01:40:28 2001 +0100
+++ b/src/HOLCF/Fun1.thy	Sat Nov 03 01:41:26 2001 +0100
@@ -1,13 +1,11 @@
 (*  Title:      HOLCF/Fun1.thy
     ID:         $Id$
     Author:     Franz Regensburger
-    Copyright   1993  Technische Universitaet Muenchen
-
+    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 !!
-
 *)
 
 Fun1 = Pcpo +
diff -r 7df1d840d01d -r 46d57d0290a2 src/HOLCF/Fun2.ML
--- a/src/HOLCF/Fun2.ML	Sat Nov 03 01:40:28 2001 +0100
+++ b/src/HOLCF/Fun2.ML	Sat Nov 03 01:41:26 2001 +0100
@@ -1,7 +1,7 @@
 (*  Title:      HOLCF/Fun2.ML
     ID:         $Id$
     Author:     Franz Regensburger
-    Copyright   1993 Technische Universitaet Muenchen
+    License:    GPL (GNU GENERAL PUBLIC LICENSE)
 
 Class Instance =>::(term,po)po
 *)
diff -r 7df1d840d01d -r 46d57d0290a2 src/HOLCF/Fun2.thy
--- a/src/HOLCF/Fun2.thy	Sat Nov 03 01:40:28 2001 +0100
+++ b/src/HOLCF/Fun2.thy	Sat Nov 03 01:41:26 2001 +0100
@@ -1,7 +1,7 @@
 (*  Title:      HOLCF/Fun2.thy
     ID:         $Id$
     Author:     Franz Regensburger
-    Copyright   1993 Technische Universitaet Muenchen
+    License:    GPL (GNU GENERAL PUBLIC LICENSE)
 
 Class Instance =>::(term,po)po
 *)
diff -r 7df1d840d01d -r 46d57d0290a2 src/HOLCF/Fun3.ML
--- a/src/HOLCF/Fun3.ML	Sat Nov 03 01:40:28 2001 +0100
+++ b/src/HOLCF/Fun3.ML	Sat Nov 03 01:41:26 2001 +0100
@@ -1,7 +1,7 @@
 (*  Title:      HOLCF/Fun3.ML
     ID:         $Id$
     Author:     Franz Regensburger
-    Copyright   1993 Technische Universitaet Muenchen
+    License:    GPL (GNU GENERAL PUBLIC LICENSE)
 *)
 
 (* for compatibility with old HOLCF-Version *)
diff -r 7df1d840d01d -r 46d57d0290a2 src/HOLCF/Fun3.thy
--- a/src/HOLCF/Fun3.thy	Sat Nov 03 01:40:28 2001 +0100
+++ b/src/HOLCF/Fun3.thy	Sat Nov 03 01:41:26 2001 +0100
@@ -1,10 +1,9 @@
 (*  Title:      HOLCF/Fun3.thy
     ID:         $Id$
     Author:     Franz Regensburger
-    Copyright   1993 Technische Universitaet Muenchen
+    License:    GPL (GNU GENERAL PUBLIC LICENSE)
 
 Class instance of  => (fun) for class pcpo
-
 *)
 
 Fun3 = Fun2 +
diff -r 7df1d840d01d -r 46d57d0290a2 src/HOLCF/HOLCF.ML
--- a/src/HOLCF/HOLCF.ML	Sat Nov 03 01:40:28 2001 +0100
+++ b/src/HOLCF/HOLCF.ML	Sat Nov 03 01:41:26 2001 +0100
@@ -1,7 +1,7 @@
 (*  Title:      HOLCF/HOLCF.ML
     ID:         $Id$
     Author:     Franz Regensburger
-    Copyright   1993 Technische Universitaet Muenchen
+    License:    GPL (GNU GENERAL PUBLIC LICENSE)
 *)
 
 use"adm.ML";
diff -r 7df1d840d01d -r 46d57d0290a2 src/HOLCF/HOLCF.thy
--- a/src/HOLCF/HOLCF.thy	Sat Nov 03 01:40:28 2001 +0100
+++ b/src/HOLCF/HOLCF.thy	Sat Nov 03 01:41:26 2001 +0100
@@ -1,11 +1,9 @@
 (*  Title:      HOLCF/HOLCF.thy
     ID:         $Id$
     Author:     Franz Regensburger
-    Copyright   1993 Technische Universitaet Muenchen
-
+    License:    GPL (GNU GENERAL PUBLIC LICENSE)
 
-Top theory for HOLCF system
-
+Top theory for HOLCF system.
 *)
 
 HOLCF = Sprod3 + Ssum3 + Up3 + Lift + Discrete + One + Tr
diff -r 7df1d840d01d -r 46d57d0290a2 src/HOLCF/One.ML
--- a/src/HOLCF/One.ML	Sat Nov 03 01:40:28 2001 +0100
+++ b/src/HOLCF/One.ML	Sat Nov 03 01:41:26 2001 +0100
@@ -1,9 +1,9 @@
 (*  Title:      HOLCF/One.ML
     ID:         $Id$
     Author:     Oscar Slotosch
-    Copyright   1997 Technische Universitaet Muenchen
+    License:    GPL (GNU GENERAL PUBLIC LICENSE)
 
-The unit domain
+The unit domain.
 *)
 
 (* ------------------------------------------------------------------------ *)
@@ -11,7 +11,7 @@
 (* ------------------------------------------------------------------------ *)
 
 Goalw [ONE_def] "t=UU | t = ONE";
-by (lift.induct_tac "t" 1);
+by (induct_tac "t" 1);
 by (Simp_tac 1);
 by (Simp_tac 1);
 qed "Exh_one";
diff -r 7df1d840d01d -r 46d57d0290a2 src/HOLCF/One.thy
--- a/src/HOLCF/One.thy	Sat Nov 03 01:40:28 2001 +0100
+++ b/src/HOLCF/One.thy	Sat Nov 03 01:41:26 2001 +0100
@@ -1,7 +1,7 @@
 (*  Title:      HOLCF/One.thy
     ID:         $Id$
     Author:     Oscar Slotosch
-    Copyright   1997 Technische Universitaet Muenchen
+    License:    GPL (GNU GENERAL PUBLIC LICENSE)
 *)
 
 One = Lift +
diff -r 7df1d840d01d -r 46d57d0290a2 src/HOLCF/Pcpo.ML
--- a/src/HOLCF/Pcpo.ML	Sat Nov 03 01:40:28 2001 +0100
+++ b/src/HOLCF/Pcpo.ML	Sat Nov 03 01:41:26 2001 +0100
@@ -1,7 +1,7 @@
 (*  Title:      HOLCF/Pcpo.ML
     ID:         $Id$
     Author:     Franz Regensburger
-    Copyright   1993 Technische Universitaet Muenchen
+    License:    GPL (GNU GENERAL PUBLIC LICENSE)
 
 introduction of the classes cpo and pcpo 
 *)
diff -r 7df1d840d01d -r 46d57d0290a2 src/HOLCF/Pcpo.thy
--- a/src/HOLCF/Pcpo.thy	Sat Nov 03 01:40:28 2001 +0100
+++ b/src/HOLCF/Pcpo.thy	Sat Nov 03 01:41:26 2001 +0100
@@ -1,7 +1,7 @@
 (*  Title:      HOLCF/Pcpo.thy
     ID:         $Id$
     Author:     Franz Regensburger
-    Copyright   1993 Technische Universitaet Muenchen
+    License:    GPL (GNU GENERAL PUBLIC LICENSE)
 
 introduction of the classes cpo and pcpo 
 *)
diff -r 7df1d840d01d -r 46d57d0290a2 src/HOLCF/Porder.ML
--- a/src/HOLCF/Porder.ML	Sat Nov 03 01:40:28 2001 +0100
+++ b/src/HOLCF/Porder.ML	Sat Nov 03 01:41:26 2001 +0100
@@ -1,7 +1,7 @@
 (*  Title:      HOLCF/Porder
     ID:         $Id$
     Author:     Franz Regensburger
-    Copyright   1993 Technische Universitaet Muenchen
+    License:    GPL (GNU GENERAL PUBLIC LICENSE)
 
 Conservative extension of theory Porder0 by constant definitions 
 *)
diff -r 7df1d840d01d -r 46d57d0290a2 src/HOLCF/Porder.thy
--- a/src/HOLCF/Porder.thy	Sat Nov 03 01:40:28 2001 +0100
+++ b/src/HOLCF/Porder.thy	Sat Nov 03 01:41:26 2001 +0100
@@ -1,10 +1,9 @@
 (*  Title:      HOLCF/porder.thy
     ID:         $Id$
     Author:     Franz Regensburger
-    Copyright   1993 Technische Universitaet Muenchen
+    License:    GPL (GNU GENERAL PUBLIC LICENSE)
 
 Conservative extension of theory Porder0 by constant definitions 
-
 *)
 
 Porder = Porder0 +
diff -r 7df1d840d01d -r 46d57d0290a2 src/HOLCF/Porder0.ML
--- a/src/HOLCF/Porder0.ML	Sat Nov 03 01:40:28 2001 +0100
+++ b/src/HOLCF/Porder0.ML	Sat Nov 03 01:41:26 2001 +0100
@@ -1,9 +1,9 @@
 (*  Title:      HOLCF/Porder0.ML
     ID:         $Id$
     Author:     Oscar Slotosch
-    Copyright   1997 Technische Universitaet Muenchen
+    License:    GPL (GNU GENERAL PUBLIC LICENSE)
 
-    derive the characteristic axioms for the characteristic constants 
+derive the characteristic axioms for the characteristic constants 
 *)
 
 AddIffs [refl_less];
diff -r 7df1d840d01d -r 46d57d0290a2 src/HOLCF/Porder0.thy
--- a/src/HOLCF/Porder0.thy	Sat Nov 03 01:40:28 2001 +0100
+++ b/src/HOLCF/Porder0.thy	Sat Nov 03 01:41:26 2001 +0100
@@ -1,10 +1,9 @@
 (*  Title:      HOLCF/Porder0.thy
     ID:         $Id$
     Author:     Franz Regensburger
-    Copyright   1993 Technische Universitaet Muenchen
+    License:    GPL (GNU GENERAL PUBLIC LICENSE)
 
-Definition of class porder (partial order)
-
+Definition of class porder (partial order).
 *)
 
 Porder0 = Main +
diff -r 7df1d840d01d -r 46d57d0290a2 src/HOLCF/Sprod0.ML
--- a/src/HOLCF/Sprod0.ML	Sat Nov 03 01:40:28 2001 +0100
+++ b/src/HOLCF/Sprod0.ML	Sat Nov 03 01:41:26 2001 +0100
@@ -1,7 +1,7 @@
 (*  Title:      HOLCF/Sprod0
     ID:         $Id$
     Author:     Franz Regensburger
-    Copyright   1993  Technische Universitaet Muenchen
+    License:    GPL (GNU GENERAL PUBLIC LICENSE)
 
 Strict product with typedef.
 *)
diff -r 7df1d840d01d -r 46d57d0290a2 src/HOLCF/Sprod0.thy
--- a/src/HOLCF/Sprod0.thy	Sat Nov 03 01:40:28 2001 +0100
+++ b/src/HOLCF/Sprod0.thy	Sat Nov 03 01:41:26 2001 +0100
@@ -1,7 +1,7 @@
 (*  Title:      HOLCF/Sprod0.thy
     ID:         $Id$
     Author:     Franz Regensburger
-    Copyright   1993  Technische Universitaet Muenchen
+    License:    GPL (GNU GENERAL PUBLIC LICENSE)
 
 Strict product with typedef.
 *)
diff -r 7df1d840d01d -r 46d57d0290a2 src/HOLCF/Sprod1.ML
--- a/src/HOLCF/Sprod1.ML	Sat Nov 03 01:40:28 2001 +0100
+++ b/src/HOLCF/Sprod1.ML	Sat Nov 03 01:41:26 2001 +0100
@@ -1,8 +1,7 @@
 (*  Title:      HOLCF/Sprod1.ML
     ID:         $Id$
     Author:     Franz Regensburger
-    Copyright   1993  Technische Universitaet Muenchen
-
+    License:    GPL (GNU GENERAL PUBLIC LICENSE)
 *)
 
 (* ------------------------------------------------------------------------ *)
diff -r 7df1d840d01d -r 46d57d0290a2 src/HOLCF/Sprod1.thy
--- a/src/HOLCF/Sprod1.thy	Sat Nov 03 01:40:28 2001 +0100
+++ b/src/HOLCF/Sprod1.thy	Sat Nov 03 01:41:26 2001 +0100
@@ -1,9 +1,9 @@
 (*  Title:      HOLCF/sprod1.thy
     ID:         $Id$
     Author:     Franz Regensburger
-    Copyright   1993  Technische Universitaet Muenchen
+    License:    GPL (GNU GENERAL PUBLIC LICENSE)
 
-Partial ordering for the strict product
+Partial ordering for the strict product.
 *)
 
 Sprod1 = Sprod0 +
diff -r 7df1d840d01d -r 46d57d0290a2 src/HOLCF/Sprod2.ML
--- a/src/HOLCF/Sprod2.ML	Sat Nov 03 01:40:28 2001 +0100
+++ b/src/HOLCF/Sprod2.ML	Sat Nov 03 01:41:26 2001 +0100
@@ -1,7 +1,7 @@
 (*  Title:      HOLCF/Sprod2.ML
     ID:         $Id$
     Author:     Franz Regensburger
-    Copyright   1993 Technische Universitaet Muenchen
+    License:    GPL (GNU GENERAL PUBLIC LICENSE)
 
 Class Instance **::(pcpo,pcpo)po
 *)
diff -r 7df1d840d01d -r 46d57d0290a2 src/HOLCF/Sprod2.thy
--- a/src/HOLCF/Sprod2.thy	Sat Nov 03 01:40:28 2001 +0100
+++ b/src/HOLCF/Sprod2.thy	Sat Nov 03 01:41:26 2001 +0100
@@ -1,7 +1,7 @@
 (*  Title:      HOLCF/Sprod2.thy
     ID:         $Id$
     Author:     Franz Regensburger
-    Copyright   1993 Technische Universitaet Muenchen
+    License:    GPL (GNU GENERAL PUBLIC LICENSE)
 
 Class Instance **::(pcpo,pcpo)po
 *)
diff -r 7df1d840d01d -r 46d57d0290a2 src/HOLCF/Sprod3.ML
--- a/src/HOLCF/Sprod3.ML	Sat Nov 03 01:40:28 2001 +0100
+++ b/src/HOLCF/Sprod3.ML	Sat Nov 03 01:41:26 2001 +0100
@@ -1,7 +1,7 @@
 (*  Title:      HOLCF/Sprod3
     ID:         $Id$
     Author:     Franz Regensburger
-    Copyright   1993 Technische Universitaet Muenchen
+    License:    GPL (GNU GENERAL PUBLIC LICENSE)
 
 Class instance of  ** for class pcpo
 *)
diff -r 7df1d840d01d -r 46d57d0290a2 src/HOLCF/Sprod3.thy
--- a/src/HOLCF/Sprod3.thy	Sat Nov 03 01:40:28 2001 +0100
+++ b/src/HOLCF/Sprod3.thy	Sat Nov 03 01:41:26 2001 +0100
@@ -1,7 +1,7 @@
 (*  Title:      HOLCF/sprod3.thy
     ID:         $Id$
     Author:     Franz Regensburger
-    Copyright   1993 Technische Universitaet Muenchen
+    License:    GPL (GNU GENERAL PUBLIC LICENSE)
 
 Class instance of  ** for class pcpo
 *)
diff -r 7df1d840d01d -r 46d57d0290a2 src/HOLCF/Ssum0.ML
--- a/src/HOLCF/Ssum0.ML	Sat Nov 03 01:40:28 2001 +0100
+++ b/src/HOLCF/Ssum0.ML	Sat Nov 03 01:41:26 2001 +0100
@@ -1,7 +1,7 @@
 (*  Title:      HOLCF/Ssum0.ML
     ID:         $Id$
     Author:     Franz Regensburger
-    Copyright   1993  Technische Universitaet Muenchen
+    License:    GPL (GNU GENERAL PUBLIC LICENSE)
 
 Strict sum with typedef
 *)
diff -r 7df1d840d01d -r 46d57d0290a2 src/HOLCF/Ssum0.thy
--- a/src/HOLCF/Ssum0.thy	Sat Nov 03 01:40:28 2001 +0100
+++ b/src/HOLCF/Ssum0.thy	Sat Nov 03 01:41:26 2001 +0100
@@ -1,7 +1,7 @@
 (*  Title:      HOLCF/Ssum0.thy
     ID:         $Id$
     Author:     Franz Regensburger
-    Copyright   1993  Technische Universitaet Muenchen
+    License:    GPL (GNU GENERAL PUBLIC LICENSE)
 
 Strict sum with typedef
 *)
diff -r 7df1d840d01d -r 46d57d0290a2 src/HOLCF/Ssum1.ML
--- a/src/HOLCF/Ssum1.ML	Sat Nov 03 01:40:28 2001 +0100
+++ b/src/HOLCF/Ssum1.ML	Sat Nov 03 01:41:26 2001 +0100
@@ -1,7 +1,7 @@
 (*  Title:      HOLCF/Ssum1.ML
     ID:         $Id$
     Author:     Franz Regensburger
-    Copyright   1993  Technische Universitaet Muenchen
+    License:    GPL (GNU GENERAL PUBLIC LICENSE)
 
 Partial ordering for the strict sum ++
 *)
diff -r 7df1d840d01d -r 46d57d0290a2 src/HOLCF/Ssum1.thy
--- a/src/HOLCF/Ssum1.thy	Sat Nov 03 01:40:28 2001 +0100
+++ b/src/HOLCF/Ssum1.thy	Sat Nov 03 01:41:26 2001 +0100
@@ -1,7 +1,7 @@
 (*  Title:      HOLCF/Ssum1.thy
     ID:         $Id$
     Author:     Franz Regensburger
-    Copyright   1993  Technische Universitaet Muenchen
+    License:    GPL (GNU GENERAL PUBLIC LICENSE)
 
 Partial ordering for the strict sum ++
 *)
diff -r 7df1d840d01d -r 46d57d0290a2 src/HOLCF/Ssum2.ML
--- a/src/HOLCF/Ssum2.ML	Sat Nov 03 01:40:28 2001 +0100
+++ b/src/HOLCF/Ssum2.ML	Sat Nov 03 01:41:26 2001 +0100
@@ -1,7 +1,7 @@
 (*  Title:      HOLCF/Ssum2.ML
     ID:         $Id$
     Author:     Franz Regensburger
-    Copyright   1993 Technische Universitaet Muenchen
+    License:    GPL (GNU GENERAL PUBLIC LICENSE)
 
 Class Instance ++::(pcpo,pcpo)po
 *)
diff -r 7df1d840d01d -r 46d57d0290a2 src/HOLCF/Ssum2.thy
--- a/src/HOLCF/Ssum2.thy	Sat Nov 03 01:40:28 2001 +0100
+++ b/src/HOLCF/Ssum2.thy	Sat Nov 03 01:41:26 2001 +0100
@@ -1,7 +1,7 @@
 (*  Title:      HOLCF/ssum2.thy
     ID:         $Id$
     Author:     Franz Regensburger
-    Copyright   1993 Technische Universitaet Muenchen
+    License:    GPL (GNU GENERAL PUBLIC LICENSE)
 
 Class Instance ++::(pcpo,pcpo)po
 *)
diff -r 7df1d840d01d -r 46d57d0290a2 src/HOLCF/Ssum3.ML
--- a/src/HOLCF/Ssum3.ML	Sat Nov 03 01:40:28 2001 +0100
+++ b/src/HOLCF/Ssum3.ML	Sat Nov 03 01:41:26 2001 +0100
@@ -1,7 +1,7 @@
 (*  Title:      HOLCF/Ssum3.ML
     ID:         $Id$
     Author:     Franz Regensburger
-    Copyright   1993 Technische Universitaet Muenchen
+    License:    GPL (GNU GENERAL PUBLIC LICENSE)
 
 Class instance of  ++ for class pcpo
 *)
diff -r 7df1d840d01d -r 46d57d0290a2 src/HOLCF/Ssum3.thy
--- a/src/HOLCF/Ssum3.thy	Sat Nov 03 01:40:28 2001 +0100
+++ b/src/HOLCF/Ssum3.thy	Sat Nov 03 01:41:26 2001 +0100
@@ -1,7 +1,7 @@
 (*  Title:      HOLCF/ssum3.thy
     ID:         $Id$
     Author:     Franz Regensburger
-    Copyright   1993 Technische Universitaet Muenchen
+    License:    GPL (GNU GENERAL PUBLIC LICENSE)
 
 Class instance of  ++ for class pcpo
 *)
diff -r 7df1d840d01d -r 46d57d0290a2 src/HOLCF/Tr.ML
--- a/src/HOLCF/Tr.ML	Sat Nov 03 01:40:28 2001 +0100
+++ b/src/HOLCF/Tr.ML	Sat Nov 03 01:41:26 2001 +0100
@@ -1,7 +1,7 @@
 (*  Title:      HOLCF/Tr.ML
     ID:         $Id$
     Author:     Franz Regensburger
-    Copyright   1993 Technische Universitaet Muenchen
+    License:    GPL (GNU GENERAL PUBLIC LICENSE)
 
 Introduce infix if_then_else_fi and boolean connectives andalso, orelse
 *)
@@ -11,7 +11,7 @@
 (* ------------------------------------------------------------------------ *)
 
 Goalw [FF_def,TT_def] "t=UU | t = TT | t = FF";
-by (lift.induct_tac "t" 1);
+by (induct_tac "t" 1);
 by (fast_tac HOL_cs 1);
 by (fast_tac (HOL_cs addss simpset()) 1);
 qed "Exh_tr";
diff -r 7df1d840d01d -r 46d57d0290a2 src/HOLCF/Tr.thy
--- a/src/HOLCF/Tr.thy	Sat Nov 03 01:40:28 2001 +0100
+++ b/src/HOLCF/Tr.thy	Sat Nov 03 01:41:26 2001 +0100
@@ -1,7 +1,7 @@
 (*  Title:      HOLCF/Tr.thy
     ID:         $Id$
     Author:     Franz Regensburger
-    Copyright   1993 Technische Universitaet Muenchen
+    License:    GPL (GNU GENERAL PUBLIC LICENSE)
 
 Introduce infix if_then_else_fi and boolean connectives andalso, orelse
 *)
diff -r 7df1d840d01d -r 46d57d0290a2 src/HOLCF/Up1.ML
--- a/src/HOLCF/Up1.ML	Sat Nov 03 01:40:28 2001 +0100
+++ b/src/HOLCF/Up1.ML	Sat Nov 03 01:41:26 2001 +0100
@@ -1,9 +1,9 @@
 (*  Title:      HOLCF/Up1.ML
     ID:         $Id$
     Author:     Franz Regensburger
-    Copyright   1993  Technische Universitaet Muenchen
+    License:    GPL (GNU GENERAL PUBLIC LICENSE)
 
-Lifting
+Lifting.
 *)
 
 Goal "Rep_Up (Abs_Up y) = y";
diff -r 7df1d840d01d -r 46d57d0290a2 src/HOLCF/Up1.thy
--- a/src/HOLCF/Up1.thy	Sat Nov 03 01:40:28 2001 +0100
+++ b/src/HOLCF/Up1.thy	Sat Nov 03 01:41:26 2001 +0100
@@ -1,11 +1,9 @@
 (*  Title:      HOLCF/Up1.thy
     ID:         $Id$
     Author:     Franz Regensburger
-    Copyright   1993  Technische Universitaet Muenchen
-
+    License:    GPL (GNU GENERAL PUBLIC LICENSE)
 
-Lifting
-
+Lifting.
 *)
 
 Up1 = Cfun3 + Sum_Type + Datatype +
diff -r 7df1d840d01d -r 46d57d0290a2 src/HOLCF/Up2.ML
--- a/src/HOLCF/Up2.ML	Sat Nov 03 01:40:28 2001 +0100
+++ b/src/HOLCF/Up2.ML	Sat Nov 03 01:41:26 2001 +0100
@@ -1,7 +1,7 @@
 (*  Title:      HOLCF/Up2.ML
     ID:         $Id$
     Author:     Franz Regensburger
-    Copyright   1993 Technische Universitaet Muenchen
+    License:    GPL (GNU GENERAL PUBLIC LICENSE)
 
 Class Instance u::(pcpo)po
 *)
diff -r 7df1d840d01d -r 46d57d0290a2 src/HOLCF/Up2.thy
--- a/src/HOLCF/Up2.thy	Sat Nov 03 01:40:28 2001 +0100
+++ b/src/HOLCF/Up2.thy	Sat Nov 03 01:41:26 2001 +0100
@@ -1,10 +1,9 @@
 (*  Title:      HOLCF/Up2.thy
     ID:         $Id$
     Author:     Franz Regensburger
-    Copyright   1993 Technische Universitaet Muenchen
+    License:    GPL (GNU GENERAL PUBLIC LICENSE)
 
 Class Instance u::(pcpo)po
-
 *)
 
 Up2 = Up1 + 
diff -r 7df1d840d01d -r 46d57d0290a2 src/HOLCF/Up3.ML
--- a/src/HOLCF/Up3.ML	Sat Nov 03 01:40:28 2001 +0100
+++ b/src/HOLCF/Up3.ML	Sat Nov 03 01:41:26 2001 +0100
@@ -1,7 +1,7 @@
 (*  Title:      HOLCF/Up3.ML
     ID:         $Id$
     Author:     Franz Regensburger
-    Copyright   1993 Technische Universitaet Muenchen
+    License:    GPL (GNU GENERAL PUBLIC LICENSE)
 
 Class instance of  ('a)u for class pcpo
 *)
diff -r 7df1d840d01d -r 46d57d0290a2 src/HOLCF/Up3.thy
--- a/src/HOLCF/Up3.thy	Sat Nov 03 01:40:28 2001 +0100
+++ b/src/HOLCF/Up3.thy	Sat Nov 03 01:41:26 2001 +0100
@@ -1,11 +1,9 @@
 (*  Title:      HOLCF/Up3.thy
     ID:         $Id$
     Author:     Franz Regensburger
-    Copyright   1993 Technische Universitaet Muenchen
-
+    License:    GPL (GNU GENERAL PUBLIC LICENSE)
 
 Class instance of  ('a)u for class pcpo
-
 *)
 
 Up3 = Up2 +
diff -r 7df1d840d01d -r 46d57d0290a2 src/HOLCF/cont_consts.ML
--- a/src/HOLCF/cont_consts.ML	Sat Nov 03 01:40:28 2001 +0100
+++ b/src/HOLCF/cont_consts.ML	Sat Nov 03 01:41:26 2001 +0100
@@ -1,6 +1,7 @@
 (*  Title:      HOLCF/cont_consts.ML
     ID:         $Id$
     Author:     Tobias Mayr and David von Oheimb
+    License:    GPL (GNU GENERAL PUBLIC LICENSE)
 
 Theory extender for consts section.
 *)
diff -r 7df1d840d01d -r 46d57d0290a2 src/HOLCF/domain/axioms.ML
--- a/src/HOLCF/domain/axioms.ML	Sat Nov 03 01:40:28 2001 +0100
+++ b/src/HOLCF/domain/axioms.ML	Sat Nov 03 01:41:26 2001 +0100
@@ -1,9 +1,9 @@
 (*  Title:      HOLCF/domain/axioms.ML
     ID:         $Id$
-    Author : David von Oheimb
-    Copyright 1995, 1996 TU Muenchen
+    Author:     David von Oheimb
+    License:    GPL (GNU GENERAL PUBLIC LICENSE)
 
-syntax generator for domain section
+Syntax generator for domain section.
 *)
 
 structure Domain_Axioms = struct
diff -r 7df1d840d01d -r 46d57d0290a2 src/HOLCF/domain/extender.ML
--- a/src/HOLCF/domain/extender.ML	Sat Nov 03 01:40:28 2001 +0100
+++ b/src/HOLCF/domain/extender.ML	Sat Nov 03 01:41:26 2001 +0100
@@ -1,7 +1,7 @@
 (*  Title:      HOLCF/domain/extender.ML
     ID:         $Id$
-    Author : David von Oheimb
-    Copyright 1995, 1996 TU Muenchen
+    Author:     David von Oheimb
+    License:    GPL (GNU GENERAL PUBLIC LICENSE)
 
 Theory extender for domain section.
 *)
diff -r 7df1d840d01d -r 46d57d0290a2 src/HOLCF/domain/interface.ML
--- a/src/HOLCF/domain/interface.ML	Sat Nov 03 01:40:28 2001 +0100
+++ b/src/HOLCF/domain/interface.ML	Sat Nov 03 01:41:26 2001 +0100
@@ -1,9 +1,9 @@
 (*  Title:      HOLCF/domain/interface.ML
     ID:         $Id$
-    Author : David von Oheimb
-    Copyright 1995, 1996 TU Muenchen
+    Author:     David von Oheimb
+    License:    GPL (GNU GENERAL PUBLIC LICENSE)
 
-parser for domain section
+Parser for domain section.
 *)
 
 local 
diff -r 7df1d840d01d -r 46d57d0290a2 src/HOLCF/domain/library.ML
--- a/src/HOLCF/domain/library.ML	Sat Nov 03 01:40:28 2001 +0100
+++ b/src/HOLCF/domain/library.ML	Sat Nov 03 01:41:26 2001 +0100
@@ -1,9 +1,9 @@
 (*  Title:      HOLCF/domain/library.ML
     ID:         $Id$
-    Author : David von Oheimb
-    Copyright 1995, 1996 TU Muenchen
+    Author:     David von Oheimb
+    License:    GPL (GNU GENERAL PUBLIC LICENSE)
 
-library for domain section
+Library for domain section.
 *)
 
 
diff -r 7df1d840d01d -r 46d57d0290a2 src/HOLCF/domain/syntax.ML
--- a/src/HOLCF/domain/syntax.ML	Sat Nov 03 01:40:28 2001 +0100
+++ b/src/HOLCF/domain/syntax.ML	Sat Nov 03 01:41:26 2001 +0100
@@ -1,9 +1,9 @@
 (*  Title:      HOLCF/domain/syntax.ML
     ID:         $Id$
-    Author : David von Oheimb
-    Copyright 1995, 1996 TU Muenchen
+    Author:     David von Oheimb
+    License:    GPL (GNU GENERAL PUBLIC LICENSE)
 
-syntax generator for domain section
+Syntax generator for domain section.
 *)
 
 structure Domain_Syntax = struct 
diff -r 7df1d840d01d -r 46d57d0290a2 src/HOLCF/domain/theorems.ML
--- a/src/HOLCF/domain/theorems.ML	Sat Nov 03 01:40:28 2001 +0100
+++ b/src/HOLCF/domain/theorems.ML	Sat Nov 03 01:41:26 2001 +0100
@@ -1,9 +1,9 @@
 (*  Title:      HOLCF/domain/theorems.ML
     ID:         $Id$
-    Author : David von Oheimb
-    Copyright 1995, 1996 TU Muenchen
+    Author:     David von Oheimb
+    License:    GPL (GNU GENERAL PUBLIC LICENSE)
 
-proof generator for domain section
+Proof generator for domain section.
 *)
 
 
diff -r 7df1d840d01d -r 46d57d0290a2 src/HOLCF/holcf_logic.ML
--- a/src/HOLCF/holcf_logic.ML	Sat Nov 03 01:40:28 2001 +0100
+++ b/src/HOLCF/holcf_logic.ML	Sat Nov 03 01:41:26 2001 +0100
@@ -1,6 +1,7 @@
 (*  Title:      HOLCF/holcf_logic.ML
     ID:         $Id$
     Author:     David von Oheimb
+    License:    GPL (GNU GENERAL PUBLIC LICENSE)
 
 Abstract syntax operations for HOLCF.
 *)
@@ -31,11 +32,7 @@
 structure HOLCFLogic: HOLCF_LOGIC =
 struct
 
-local
-
-  open HOLogic;
-
-in
+open HOLogic;
 
 fun mk_btyp t (S,T) = Type (t,[S,T]);
 val mk_prodT = mk_btyp "*";
@@ -62,5 +59,4 @@
 val oneT      = Type (intern "one",[ ]);
 end;
 
-end; (* local *)
-end; (* struct *)
+end;