src/HOLCF/Lift2.thy

--- a/src/HOLCF/Lift2.thy	Sat Feb 15 18:24:05 1997 +0100
+++ b/src/HOLCF/Lift2.thy	Mon Feb 17 10:57:11 1997 +0100
@@ -8,13 +8,8 @@
 
 Lift2 = Lift1 + 
 
-default term
-
-arities "lift" :: (term)po
-
-rules
-
- inst_lift_po   "((op <<)::['a lift,'a lift]=>bool) = less_lift"
+instance "lift" :: (term)po (refl_less_lift,antisym_less_lift,trans_less_lift)
 
 end
 
+