--- a/src/HOLCF/FOCUS/Fstreams.thy Thu Jan 17 00:51:20 2008 +0100
+++ b/src/HOLCF/FOCUS/Fstreams.thy Thu Jan 17 21:44:19 2008 +0100
@@ -264,7 +264,7 @@
apply (subgoal_tac "Y ja << (LUB i. (Y i))", clarsimp)
apply (drule fstreams_mono, simp)
apply (rule is_ub_thelub, simp)
-apply (blast intro: chain_mono3)
+apply (blast intro: chain_mono)
by (rule stream_reach2)
@@ -285,7 +285,7 @@
apply (case_tac "Y j", auto)
apply (rule_tac x="j" in exI)
apply (case_tac "Y j",auto)
-by (drule chain_mono3, auto)
+by (drule chain_mono, auto)
lemma fstreams_lub_lemma2:
"[| chain Y; lub (range Y) = (a, <m> ooo ms); (a::'a::flat) ~= UU |] ==> EX j t. Y j = (a, <m> ooo t)"
@@ -328,7 +328,7 @@
apply (subgoal_tac "fst (Y j) ~= fst (Y ja) | snd (Y j) ~= snd (Y ja)", simp)
apply (drule ax_flat, simp)+
apply (drule prod_eqI, auto)
-apply (simp add: chain_mono3)
+apply (simp add: chain_mono)
by (rule stream_reach2)