src/HOLCF/Lift1.thy

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOLCF/Lift1.thy	Mon Dec 09 19:16:20 1996 +0100
@@ -0,0 +1,18 @@
+Lift1 = Tr2 + 
+
+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)"
+
+
+end
+