moved Lift*.* to Up*.*, renaming of all constans and theorems concerned,
(*lift* to *up*, except Ilift to Ifup, lift to fup)
--- a/src/HOLCF/explicit_domains/Dnat.ML Fri Nov 29 12:16:57 1996 +0100
+++ b/src/HOLCF/explicit_domains/Dnat.ML Fri Nov 29 12:17:30 1996 +0100
@@ -499,7 +499,7 @@
]);
-qed_goalw "dnat_flat" Dnat.thy [is_flat_def] "is_flat(dzero)"
+qed_goalw "dnat_flat" Dnat.thy [flat_def] "flat(dzero)"
(fn prems =>
[
(rtac allI 1),
--- a/src/HOLCF/explicit_domains/Stream.ML Fri Nov 29 12:16:57 1996 +0100
+++ b/src/HOLCF/explicit_domains/Stream.ML Fri Nov 29 12:17:30 1996 +0100
@@ -52,7 +52,7 @@
(res_inst_tac [("p","stream_rep`s")] sprodE 1),
(asm_simp_tac (!simpset addsimps stream_rews) 1),
(Asm_simp_tac 1),
- (res_inst_tac [("p","y")] liftE1 1),
+ (res_inst_tac [("p","y")] upE1 1),
(contr_tac 1),
(rtac disjI2 1),
(rtac exI 1),
--- a/src/HOLCF/explicit_domains/Stream.thy Fri Nov 29 12:16:57 1996 +0100
+++ b/src/HOLCF/explicit_domains/Stream.thy Fri Nov 29 12:17:30 1996 +0100
@@ -65,7 +65,7 @@
stream_abs_iso "stream_rep`(stream_abs`x) = x"
stream_rep_iso "stream_abs`(stream_rep`x) = x"
stream_copy_def "stream_copy == (LAM f. stream_abs oo
- (ssplit`(LAM x y. (|x , (lift`(up oo f))`y|) )) oo stream_rep)"
+ (ssplit`(LAM x y. (|x , (fup`(up oo f))`y|) )) oo stream_rep)"
stream_reach "(fix`stream_copy)`x = x"
defs
@@ -80,7 +80,7 @@
(* discriminator functional *)
stream_when_def
-"stream_when == (LAM f l.ssplit `(LAM x l.f`x`(lift`ID`l)) `(stream_rep`l))"
+"stream_when == (LAM f l.ssplit `(LAM x l.f`x`(fup`ID`l)) `(stream_rep`l))"
(* ----------------------------------------------------------------------- *)
(* discriminators and selectors *)