--- a/src/HOLCF/FOCUS/Fstream.thy Wed Nov 03 15:31:24 2010 -0700
+++ b/src/HOLCF/FOCUS/Fstream.thy Wed Nov 03 15:47:46 2010 -0700
@@ -94,7 +94,7 @@
apply (rule lift.exhaust)
apply (erule (1) notE)
apply (safe)
-apply (drule Def_inject_less_eq [THEN iffD1])
+apply (drule Def_below_Def [THEN iffD1])
apply fast
done
--- 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)
--- a/src/HOLCF/FOCUS/Stream_adm.thy Wed Nov 03 15:31:24 2010 -0700
+++ b/src/HOLCF/FOCUS/Stream_adm.thy Wed Nov 03 15:47:46 2010 -0700
@@ -157,7 +157,7 @@
apply ( fast)
apply (unfold linorder_not_less)
apply (drule (1) mp)
-apply (erule all_dupE, drule mp, rule refl_less)
+apply (erule all_dupE, drule mp, rule below_refl)
apply (erule ssubst)
apply (erule allE, drule (1) mp)
apply (drule_tac P="%x. x" in subst, assumption)
--- a/src/HOLCF/HOLCF.thy Wed Nov 03 15:31:24 2010 -0700
+++ b/src/HOLCF/HOLCF.thy Wed Nov 03 15:47:46 2010 -0700
@@ -31,52 +31,4 @@
lemmas cont_Rep_CFun_app = cont_APP_app
lemmas cont_Rep_CFun_app_app = cont_APP_app_app
-text {* Older legacy theorem names: *}
-
-lemmas sq_ord_less_eq_trans = below_eq_trans
-lemmas sq_ord_eq_less_trans = eq_below_trans
-lemmas refl_less = below_refl
-lemmas trans_less = below_trans
-lemmas antisym_less = below_antisym
-lemmas antisym_less_inverse = below_antisym_inverse
-lemmas box_less = box_below
-lemmas rev_trans_less = rev_below_trans
-lemmas not_less2not_eq = not_below2not_eq
-lemmas less_UU_iff = below_UU_iff
-lemmas flat_less_iff = flat_below_iff
-lemmas adm_less = adm_below
-lemmas adm_not_less = adm_not_below
-lemmas adm_compact_not_less = adm_compact_not_below
-lemmas less_fun_def = below_fun_def
-lemmas expand_fun_less = expand_fun_below
-lemmas less_fun_ext = below_fun_ext
-lemmas less_discr_def = below_discr_def
-lemmas discr_less_eq = discr_below_eq
-lemmas less_unit_def = below_unit_def
-lemmas less_cprod_def = below_prod_def
-lemmas prod_lessI = prod_belowI
-lemmas Pair_less_iff = Pair_below_iff
-lemmas fst_less_iff = fst_below_iff
-lemmas snd_less_iff = snd_below_iff
-lemmas expand_cfun_less = expand_cfun_below
-lemmas less_cfun_ext = below_cfun_ext
-lemmas injection_less = injection_below
-lemmas less_up_def = below_up_def
-lemmas not_Iup_less = not_Iup_below
-lemmas Iup_less = Iup_below
-lemmas up_less = up_below
-lemmas Def_inject_less_eq = Def_below_Def
-lemmas Def_less_is_eq = Def_below_iff
-lemmas spair_less_iff = spair_below_iff
-lemmas less_sprod = below_sprod
-lemmas spair_less = spair_below
-lemmas sfst_less_iff = sfst_below_iff
-lemmas ssnd_less_iff = ssnd_below_iff
-lemmas fix_least_less = fix_least_below
-lemmas dist_less_one = dist_below_one
-lemmas less_ONE = below_ONE
-lemmas ONE_less_iff = ONE_below_iff
-lemmas less_sinlD = below_sinlD
-lemmas less_sinrD = below_sinrD
-
end
--- a/src/HOLCF/IOA/meta_theory/CompoTraces.thy Wed Nov 03 15:31:24 2010 -0700
+++ b/src/HOLCF/IOA/meta_theory/CompoTraces.thy Wed Nov 03 15:47:46 2010 -0700
@@ -260,8 +260,8 @@
apply auto
(* a: act A; a: act B *)
-apply (frule sym [THEN antisym_less_inverse, THEN conjunct1, THEN divide_Seq])
-apply (frule sym [THEN antisym_less_inverse, THEN conjunct1, THEN divide_Seq])
+apply (frule sym [THEN below_antisym_inverse, THEN conjunct1, THEN divide_Seq])
+apply (frule sym [THEN below_antisym_inverse, THEN conjunct1, THEN divide_Seq])
back
apply (erule conjE)+
(* Finite (tw iA x) and Finite (tw iB y) *)
@@ -275,7 +275,7 @@
apply (simp add: not_ext_is_int_or_not_act ForallTL ForallDropwhile)
(* a: act B; a~: act A *)
-apply (frule sym [THEN antisym_less_inverse, THEN conjunct1, THEN divide_Seq])
+apply (frule sym [THEN below_antisym_inverse, THEN conjunct1, THEN divide_Seq])
apply (erule conjE)+
(* Finite (tw iB y) *)
@@ -287,7 +287,7 @@
apply (simp add: not_ext_is_int_or_not_act ForallTL ForallDropwhile)
(* a~: act B; a: act A *)
-apply (frule sym [THEN antisym_less_inverse, THEN conjunct1, THEN divide_Seq])
+apply (frule sym [THEN below_antisym_inverse, THEN conjunct1, THEN divide_Seq])
apply (erule conjE)+
(* Finite (tw iA x) *)
@@ -327,7 +327,7 @@
apply (erule conjE)+
apply simp
(* divide_Seq on s *)
-apply (frule sym [THEN antisym_less_inverse, THEN conjunct1, THEN divide_Seq])
+apply (frule sym [THEN below_antisym_inverse, THEN conjunct1, THEN divide_Seq])
apply (erule conjE)+
(* transform assumption f eB y = f B (s@z) *)
apply (drule_tac x = "y" and g = "Filter (%a. a:act B) $ (s@@z) " in subst_lemma2)
@@ -373,7 +373,7 @@
apply (erule conjE)+
apply simp
(* divide_Seq on s *)
-apply (frule sym [THEN antisym_less_inverse, THEN conjunct1, THEN divide_Seq])
+apply (frule sym [THEN below_antisym_inverse, THEN conjunct1, THEN divide_Seq])
apply (erule conjE)+
(* transform assumption f eA x = f A (s@z) *)
apply (drule_tac x = "x" and g = "Filter (%a. a:act A) $ (s@@z) " in subst_lemma2)
@@ -557,7 +557,7 @@
prefer 2 apply fast
(* bring in divide Seq for s *)
-apply (frule sym [THEN antisym_less_inverse, THEN conjunct1, THEN divide_Seq])
+apply (frule sym [THEN below_antisym_inverse, THEN conjunct1, THEN divide_Seq])
apply (erule conjE)+
(* subst divide_Seq in conclusion, but only at the righest occurence *)
@@ -610,7 +610,7 @@
prefer 2 apply (fast)
(* bring in divide Seq for s *)
-apply (frule sym [THEN antisym_less_inverse, THEN conjunct1, THEN divide_Seq])
+apply (frule sym [THEN below_antisym_inverse, THEN conjunct1, THEN divide_Seq])
apply (erule conjE)+
(* subst divide_Seq in conclusion, but only at the righest occurence *)
@@ -628,7 +628,7 @@
apply (simp add: ext_and_act)
(* divide_Seq for schB2 *)
-apply (frule_tac y = "y2" in sym [THEN antisym_less_inverse, THEN conjunct1, THEN divide_Seq])
+apply (frule_tac y = "y2" in sym [THEN below_antisym_inverse, THEN conjunct1, THEN divide_Seq])
apply (erule conjE)+
(* assumption schA *)
apply (drule_tac x = "schA" and g = "Filter (%a. a:act A) $rs" in subst_lemma2)
@@ -776,7 +776,7 @@
prefer 2 apply (fast)
(* bring in divide Seq for s *)
-apply (frule sym [THEN antisym_less_inverse, THEN conjunct1, THEN divide_Seq])
+apply (frule sym [THEN below_antisym_inverse, THEN conjunct1, THEN divide_Seq])
apply (erule conjE)+
(* subst divide_Seq in conclusion, but only at the righest occurence *)
@@ -827,7 +827,7 @@
prefer 2 apply (fast)
(* bring in divide Seq for s *)
-apply (frule sym [THEN antisym_less_inverse, THEN conjunct1, THEN divide_Seq])
+apply (frule sym [THEN below_antisym_inverse, THEN conjunct1, THEN divide_Seq])
apply (erule conjE)+
(* subst divide_Seq in conclusion, but only at the righest occurence *)
@@ -845,7 +845,7 @@
apply (simp add: ext_and_act)
(* divide_Seq for schB2 *)
-apply (frule_tac y = "x2" in sym [THEN antisym_less_inverse, THEN conjunct1, THEN divide_Seq])
+apply (frule_tac y = "x2" in sym [THEN below_antisym_inverse, THEN conjunct1, THEN divide_Seq])
apply (erule conjE)+
(* assumption schA *)
apply (drule_tac x = "schB" and g = "Filter (%a. a:act B) $rs" in subst_lemma2)
--- a/src/HOLCF/IOA/meta_theory/Sequence.thy Wed Nov 03 15:31:24 2010 -0700
+++ b/src/HOLCF/IOA/meta_theory/Sequence.thy Wed Nov 03 15:47:46 2010 -0700
@@ -293,7 +293,7 @@
lemma Cons_not_less_UU: "~(a>>x) << UU"
apply (rule notI)
-apply (drule antisym_less)
+apply (drule below_antisym)
apply simp
apply (simp add: Cons_not_UU)
done
--- a/src/HOLCF/ex/Dagstuhl.thy Wed Nov 03 15:31:24 2010 -0700
+++ b/src/HOLCF/ex/Dagstuhl.thy Wed Nov 03 15:47:46 2010 -0700
@@ -46,7 +46,7 @@
done
lemma lemma5: "y && YYS = YYS"
- apply (rule antisym_less)
+ apply (rule below_antisym)
apply (rule lemma4)
apply (rule lemma3)
done
@@ -84,7 +84,7 @@
done
lemma wir_moel': "YS = YYS"
- apply (rule antisym_less)
+ apply (rule below_antisym)
apply (rule lemma7)
apply (rule lemma6)
done
--- a/src/HOLCF/ex/Fix2.thy Wed Nov 03 15:31:24 2010 -0700
+++ b/src/HOLCF/ex/Fix2.thy Wed Nov 03 15:47:46 2010 -0700
@@ -17,7 +17,7 @@
lemma lemma1: "fix = gix"
apply (rule cfun_eqI)
-apply (rule antisym_less)
+apply (rule below_antisym)
apply (rule fix_least)
apply (rule gix1_def)
apply (rule gix2_def)