src/HOLCF/Lift1.thy

--- a/src/HOLCF/Lift1.thy	Sat Feb 15 18:24:05 1997 +0100
+++ b/src/HOLCF/Lift1.thy	Mon Feb 17 10:57:11 1997 +0100
@@ -6,21 +6,14 @@
 Lifting types of class term to flat pcpo's
 *)
 
-Lift1 = Tr2 + 
+Lift1 = ccc1 + 
 
 default term
 
 datatype 'a lift = Undef | Def 'a
 
-arities "lift" :: (term)term
-
-consts less_lift    :: "['a lift, 'a lift] => bool"
-       UU_lift      :: "'a lift"
-
 defs 
  
- less_lift_def  "less_lift x y == (x=y | x=Undef)"
-
+ less_lift_def  "less x y == (x=y | x=Undef)"
 
 end
-