--- a/src/HOLCF/FOCUS/Fstreams.thy Fri Jun 20 17:43:16 2008 +0200
+++ b/src/HOLCF/FOCUS/Fstreams.thy Fri Jun 20 17:56:00 2008 +0200
@@ -222,7 +222,7 @@
apply (case_tac "y=UU", auto)
apply (drule stream_exhaust_eq [THEN iffD1], auto)
apply (auto simp add: stream.inverts)
-apply (simp add: less_lift)
+apply (simp add: flat_less_iff)
apply (case_tac "s=UU", auto)
apply (drule stream_exhaust_eq [THEN iffD1], auto)
apply (erule_tac x="ya" in allE)
@@ -230,11 +230,11 @@
apply (case_tac "y=UU",auto)
apply (drule stream_exhaust_eq [THEN iffD1], clarsimp)
apply (auto simp add: stream.inverts)
-apply (simp add: less_lift)
+apply (simp add: flat_less_iff)
apply (erule_tac x="tt" in allE)
apply (erule_tac x="yb" in allE, auto)
-apply (simp add: less_lift)
-by (simp add: less_lift)
+apply (simp add: flat_less_iff)
+by (simp add: flat_less_iff)
lemma fstreams_lub_lemma1: "[| chain Y; lub (range Y) = <a> ooo s |] ==> EX j t. Y j = <a> ooo t"
apply (subgoal_tac "lub(range Y) ~= UU")