--- a/src/HOLCF/FOCUS/Fstreams.thy Wed Nov 03 15:31:24 2010 -0700
+++ b/src/HOLCF/FOCUS/Fstreams.thy Wed Nov 03 15:47:46 2010 -0700
@@ -217,7 +217,7 @@
apply (drule stream_exhaust_eq [THEN iffD1], auto)
apply (case_tac "y=UU", auto)
apply (drule stream_exhaust_eq [THEN iffD1], auto)
-apply (simp add: flat_less_iff)
+apply (simp add: flat_below_iff)
apply (case_tac "s=UU", auto)
apply (drule stream_exhaust_eq [THEN iffD1], auto)
apply (erule_tac x="ya" in allE)
@@ -225,11 +225,11 @@
apply (case_tac "y=UU",auto)
apply (drule stream_exhaust_eq [THEN iffD1], clarsimp)
apply auto
-apply (simp add: flat_less_iff)
+apply (simp add: flat_below_iff)
apply (erule_tac x="tt" in allE)
apply (erule_tac x="yb" in allE, auto)
-apply (simp add: flat_less_iff)
-by (simp add: flat_less_iff)
+apply (simp add: flat_below_iff)
+by (simp add: flat_below_iff)
lemma fstreams_lub_lemma1: "[| chain Y; (LUB i. Y i) = <a> ooo s |] ==> EX j t. Y j = <a> ooo t"
apply (subgoal_tac "(LUB i. Y i) ~= UU")
@@ -249,7 +249,7 @@
apply (frule lub_finch1 [THEN thelubI], auto)
apply (rule_tac x="j" in exI)
apply (erule subst) back back
-apply (simp add: less_cprod_def sconc_mono)
+apply (simp add: below_prod_def sconc_mono)
apply (simp add: max_in_chain_def, auto)
apply (rule_tac x="ja" in exI)
apply (subgoal_tac "Y j << Y ja")
@@ -274,7 +274,7 @@
apply (rule_tac x="i" in exI, auto)
apply (simp add: max_in_chain_def, auto)
apply (subgoal_tac "Y i << Y j",auto)
-apply (simp add: less_cprod_def, clarsimp)
+apply (simp add: below_prod_def, clarsimp)
apply (drule ax_flat, auto)
apply (case_tac "snd (Y j) = UU",auto)
apply (case_tac "Y j", auto)
@@ -305,8 +305,8 @@
apply (simp add: max_in_chain_def, auto)
apply (rule_tac x="ja" in exI)
apply (subgoal_tac "Y j << Y ja")
-apply (simp add: less_cprod_def, auto)
-apply (drule trans_less)
+apply (simp add: below_prod_def, auto)
+apply (drule below_trans)
apply (simp add: ax_flat, auto)
apply (drule fstreams_prefix, auto)+
apply (rule sconc_mono)
@@ -316,7 +316,7 @@
apply (subgoal_tac "snd (Y ja) << (LUB i. snd (Y i))", clarsimp)
apply (drule fstreams_mono, simp)
apply (rule is_ub_thelub chainI)
-apply (simp add: chain_def less_cprod_def)
+apply (simp add: chain_def below_prod_def)
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)