--- a/src/HOLCF/Lift3.thy Sat Feb 15 18:24:05 1997 +0100
+++ b/src/HOLCF/Lift3.thy Mon Feb 17 10:57:11 1997 +0100
@@ -8,40 +8,24 @@
Lift3 = Lift2 +
-default term
-
-arities
- "lift" :: (term)pcpo
+instance lift :: (term)pcpo (cpo_lift,least_lift)
consts
flift1 :: "('a => 'b::pcpo) => ('a lift -> 'b)"
- blift :: "bool => tr"
- plift :: "('a => bool) => 'a lift -> tr"
flift2 :: "('a => 'b) => ('a lift -> 'b lift)"
translations
"UU" <= "Undef"
defs
- blift_def
- "blift b == (if b then TT else FF)"
-
flift1_def
"flift1 f == (LAM x. (case x of
Undef => UU
| Def y => (f y)))"
-
flift2_def
"flift2 f == (LAM x. (case x of
Undef => Undef
| Def y => Def (f y)))"
- plift_def
- "plift p == (LAM x. flift1 (%a. blift (p a))`x)"
-
-
-rules
- inst_lift_pcpo "(UU::'a lift) = Undef"
-
end