# HG changeset patch
# User sandnerr
# Date 850156027 -3600
# Node ID dd2e5e655fd2231776dc95108928958950f7c9dc
# Parent  125260ef480cd09de8bb54da22fca9bb6764917e
Headers added

diff -r 125260ef480c -r dd2e5e655fd2 src/HOLCF/Lift1.ML
--- a/src/HOLCF/Lift1.ML	Mon Dec 09 19:16:20 1996 +0100
+++ b/src/HOLCF/Lift1.ML	Mon Dec 09 19:27:07 1996 +0100
@@ -1,4 +1,11 @@
-(* Lift1.ML *)
+(*  Title:      HOLCF/Lift1.ML
+    ID:         $Id$
+    Author:     Olaf Mueller, Robert Sandner
+    Copyright   1996 Technische Universitaet Muenchen
+
+Theorems for Lift1.thy
+*)
+
 
 open Lift1;
 
diff -r 125260ef480c -r dd2e5e655fd2 src/HOLCF/Lift1.thy
--- a/src/HOLCF/Lift1.thy	Mon Dec 09 19:16:20 1996 +0100
+++ b/src/HOLCF/Lift1.thy	Mon Dec 09 19:27:07 1996 +0100
@@ -1,3 +1,11 @@
+(*  Title:      HOLCF/Lift1.thy
+    ID:         $Id$
+    Author:     Olaf Mueller, Robert Sandner
+    Copyright   1996 Technische Universitaet Muenchen
+
+Lifting types of class term to flat pcpo's
+*)
+
 Lift1 = Tr2 + 
 
 default term
diff -r 125260ef480c -r dd2e5e655fd2 src/HOLCF/Lift2.ML
--- a/src/HOLCF/Lift2.ML	Mon Dec 09 19:16:20 1996 +0100
+++ b/src/HOLCF/Lift2.ML	Mon Dec 09 19:27:07 1996 +0100
@@ -1,4 +1,11 @@
- (* Lift2.ML *)
+(*  Title:      HOLCF/Lift2.ML
+    ID:         $Id$
+    Author:     Olaf Mueller, Robert Sandner
+    Copyright   1996 Technische Universitaet Muenchen
+
+Theorems for Lift2.thy
+*)
+
 
 open Lift2;
 Addsimps [less_lift_def];
diff -r 125260ef480c -r dd2e5e655fd2 src/HOLCF/Lift2.thy
--- a/src/HOLCF/Lift2.thy	Mon Dec 09 19:16:20 1996 +0100
+++ b/src/HOLCF/Lift2.thy	Mon Dec 09 19:27:07 1996 +0100
@@ -1,3 +1,11 @@
+(*  Title:      HOLCF/Lift2.thy
+    ID:         $Id$
+    Author:     Olaf Mueller, Robert Sandner
+    Copyright   1996 Technische Universitaet Muenchen
+
+Class Instance lift::(term)po
+*)
+
 Lift2 = Lift1 + 
 
 default term
diff -r 125260ef480c -r dd2e5e655fd2 src/HOLCF/Lift3.ML
--- a/src/HOLCF/Lift3.ML	Mon Dec 09 19:16:20 1996 +0100
+++ b/src/HOLCF/Lift3.ML	Mon Dec 09 19:27:07 1996 +0100
@@ -1,11 +1,14 @@
-(* Lift3.ML *)
+(*  Title:      HOLCF/Lift3.ML
+    ID:         $Id$
+    Author:     Olaf Mueller, Robert Sandner
+    Copyright   1996 Technische Universitaet Muenchen
+
+Theorems for Lift3.thy
+*)
+
 
 open Lift3;
 
-
-
-
-
 (* ----------------------------------------------------------- *)
 (*                        From Undef to UU		       *)
 (* ----------------------------------------------------------- *)
diff -r 125260ef480c -r dd2e5e655fd2 src/HOLCF/Lift3.thy
--- a/src/HOLCF/Lift3.thy	Mon Dec 09 19:16:20 1996 +0100
+++ b/src/HOLCF/Lift3.thy	Mon Dec 09 19:27:07 1996 +0100
@@ -1,3 +1,11 @@
+(*  Title:      HOLCF/Lift3.thy
+    ID:         $Id$
+    Author:     Olaf Mueller, Robert Sandner
+    Copyright   1996 Technische Universitaet Muenchen
+
+Class Instance lift::(term)pcpo
+*)
+
 Lift3 = Lift2 + 
 
 default term