--- 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;
--- 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
--- 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];
--- 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
--- 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 *)
(* ----------------------------------------------------------- *)
--- 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