# HG changeset patch
# User oheimb
# Date 849266250 -3600
# Node ID 9174de6c714373f6dacc7238572f17cb68f85bd4
# Parent  3eb9a113029e0281dc25aa19e249d8bd8d5eb4f7
moved Lift*.* to Up*.*, renaming of all constans and theorems concerned,
                        (*lift* to *up*, except Ilift to Ifup, lift to fup)

diff -r 3eb9a113029e -r 9174de6c7143 src/HOLCF/explicit_domains/Dnat.ML
--- 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),
diff -r 3eb9a113029e -r 9174de6c7143 src/HOLCF/explicit_domains/Stream.ML
--- 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),
diff -r 3eb9a113029e -r 9174de6c7143 src/HOLCF/explicit_domains/Stream.thy
--- 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                                            *)