--- a/src/HOL/Auth/KerberosIV.ML Mon Oct 07 19:01:51 2002 +0200
+++ b/src/HOL/Auth/KerberosIV.ML Tue Oct 08 08:20:17 2002 +0200
@@ -772,7 +772,6 @@
conclude AuthKey \\<noteq> AuthKeya.*)
by (Clarify_tac 9);
by analz_sees_tac;
-by (rotate_tac ~1 11);
by (ALLGOALS
(asm_full_simp_tac
(simpset() addsimps [less_SucI, new_keys_not_analzd,
@@ -800,7 +799,6 @@
by (thin_tac "Says Aa Tgs ?X \\<in> set ?evs" 1);
by (forward_tac [Says_imp_spies RS parts.Inj RS ServKey_notin_AuthKeysD] 1);
by (assume_tac 1 THEN Blast_tac 1 THEN assume_tac 1);
-by (rotate_tac ~1 1);
by (asm_full_simp_tac (simpset() addsimps [analz_insert_freshK2]) 1);
by (blast_tac (claset() addDs [Says_imp_spies RS parts.Inj, Key_unique_SesKey]
addIs [less_SucI]) 1);
--- a/src/HOL/GroupTheory/Coset.thy Mon Oct 07 19:01:51 2002 +0200
+++ b/src/HOL/GroupTheory/Coset.thy Tue Oct 08 08:20:17 2002 +0200
@@ -345,7 +345,6 @@
apply (rule inj_onI)
apply (subgoal_tac "x \<in> carrier G & y \<in> carrier G")
prefer 2 apply (blast intro: r_coset_subset_G [THEN subsetD])
-apply (rotate_tac -1)
apply (simp add: subsetD)
done
--- a/src/HOL/GroupTheory/Sylow.thy Mon Oct 07 19:01:51 2002 +0200
+++ b/src/HOL/GroupTheory/Sylow.thy Tue Oct 08 08:20:17 2002 +0200
@@ -289,7 +289,7 @@
apply (rule bexI)
apply (rule_tac [2] setrcos_H_funcset_M)
apply (rule inj_onI)
-apply (rotate_tac -2, simp)
+apply (simp)
apply (rule trans [OF _ H_elem_map_eq])
prefer 2 apply assumption
apply (rule H_elem_map_eq [symmetric, THEN trans], assumption)
--- a/src/HOL/Hyperreal/HyperDef.ML Mon Oct 07 19:01:51 2002 +0200
+++ b/src/HOL/Hyperreal/HyperDef.ML Tue Oct 08 08:20:17 2002 +0200
@@ -119,12 +119,11 @@
Goal "{n::nat. P} : FreeUltrafilterNat ==> P";
by (rtac ccontr 1);
-by (rotate_tac 1 1);
by (Asm_full_simp_tac 1);
qed "FreeUltrafilterNat_P";
Goal "{n. P(n)} : FreeUltrafilterNat ==> EX n. P(n)";
-by (rtac ccontr 1 THEN rotate_tac 1 1);
+by (rtac ccontr 1);
by (Asm_full_simp_tac 1);
qed "FreeUltrafilterNat_Ex_P";
@@ -262,7 +261,7 @@
by (dtac eq_equiv_class 1);
by (rtac equiv_hyprel 1);
by (Fast_tac 1);
-by (rtac ccontr 1 THEN rotate_tac 1 1);
+by (rtac ccontr 1);
by Auto_tac;
qed "inj_hypreal_of_real";
@@ -631,7 +630,6 @@
Goalw [hypreal_one_def,hypreal_zero_def]
"x ~= 0 ==> x*inverse(x) = (1::hypreal)";
by (res_inst_tac [("z","x")] eq_Abs_hypreal 1);
-by (rotate_tac 1 1);
by (asm_full_simp_tac (simpset() addsimps [hypreal_inverse, hypreal_mult]) 1);
by (dtac FreeUltrafilterNat_Compl_mem 1);
by (blast_tac (claset() addSIs [real_mult_inv_right,
--- a/src/HOL/Hyperreal/Lim.ML Mon Oct 07 19:01:51 2002 +0200
+++ b/src/HOL/Hyperreal/Lim.ML Tue Oct 08 08:20:17 2002 +0200
@@ -877,7 +877,6 @@
approx_mult1 1);
by (ALLGOALS(dtac (hypreal_not_eq_minus_iff RS iffD1)));
by (subgoal_tac "(*f* (%z. z - x)) u \\<noteq> (0::hypreal)" 2);
-by (rotate_tac ~1 2);
by (auto_tac (claset(),
simpset() addsimps [real_diff_def, hypreal_diff_def,
(approx_minus_iff RS iffD1) RS (mem_infmal_iff RS iffD2),
--- a/src/HOL/IMP/Compiler.thy Mon Oct 07 19:01:51 2002 +0200
+++ b/src/HOL/IMP/Compiler.thy Tue Oct 08 08:20:17 2002 +0200
@@ -97,10 +97,8 @@
apply(rule iffI)
defer apply simp
apply(subgoal_tac "n \<le> size p1")
- apply(rotate_tac -1)
apply simp
apply(rule ccontr)
-apply(rotate_tac -1)
apply(drule_tac f = length in arg_cong)
apply simp
apply arith
--- a/src/HOL/IMP/Hoare.thy Mon Oct 07 19:01:51 2002 +0200
+++ b/src/HOL/IMP/Hoare.thy Tue Oct 08 08:20:17 2002 +0200
@@ -116,9 +116,7 @@
apply (rule weak_coinduct)
apply (erule CollectI)
apply safe
- apply (rotate_tac -1)
apply simp
- apply (rotate_tac -1)
apply simp
apply (simp add: wp_def Gamma_def)
apply (intro strip)
@@ -146,8 +144,8 @@
apply (rule hoare_conseq1)
prefer 2 apply (fast)
apply safe
- apply (rotate_tac -1, simp)
-apply (rotate_tac -1, simp)
+ apply simp
+apply simp
done
lemma hoare_relative_complete: "|= {P}c{Q} ==> |- {P}c{Q}"
--- a/src/HOL/MiniML/MiniML.ML Mon Oct 07 19:01:51 2002 +0200
+++ b/src/HOL/MiniML/MiniML.ML Tue Oct 08 08:20:17 2002 +0200
@@ -90,7 +90,6 @@
by (rtac ballI 1);
by (etac UN_E 1);
by (dtac (dom_S' RS subsetD) 1);
-by (rotate_tac 1 1);
by (Asm_full_simp_tac 1);
by (fast_tac (claset() addDs [free_tv_of_substitutions_extend_to_scheme_lists]
addIs [free_tv_of_substitutions_extend_to_types RS subsetD]) 1);
--- a/src/HOL/MiniML/Type.ML Mon Oct 07 19:01:51 2002 +0200
+++ b/src/HOL/MiniML/Type.ML Tue Oct 08 08:20:17 2002 +0200
@@ -269,7 +269,6 @@
by (Simp_tac 1);
by (safe_tac (empty_cs addSIs [exI,conjI,notI]));
by (assume_tac 2);
-by (rotate_tac 1 1);
by (Asm_full_simp_tac 1);
qed "cod_app_subst";
Addsimps [cod_app_subst];
@@ -474,7 +473,6 @@
by (simp_tac (simpset() addsimps [free_tv_subst,dom_def,cod_def]) 1);
by (strip_tac 1);
by (case_tac "S nat = TVar nat" 1);
-by (rotate_tac 3 1);
by (Asm_full_simp_tac 1);
by (dres_inst_tac [("x","m")] spec 1);
by (Fast_tac 1);
--- a/src/HOL/NumberTheory/BijectionRel.thy Mon Oct 07 19:01:51 2002 +0200
+++ b/src/HOL/NumberTheory/BijectionRel.thy Tue Oct 08 08:20:17 2002 +0200
@@ -191,7 +191,6 @@
apply clarify
apply (case_tac "b \<in> F")
prefer 2
- apply (rotate_tac -1)
apply (simp add: subset_insert)
apply (cut_tac F = F and a = b and A = A and B = B in aux1)
prefer 6
@@ -205,7 +204,6 @@
apply clarify
apply (case_tac "a \<in> F")
apply (case_tac [!] "b \<in> F")
- apply (rotate_tac [2-4] -2)
apply (cut_tac F = F and a = a and b = b and A = A and B = B
in aux2)
apply (simp_all add: subset_insert)
--- a/src/HOL/NumberTheory/IntPrimes.thy Mon Oct 07 19:01:51 2002 +0200
+++ b/src/HOL/NumberTheory/IntPrimes.thy Tue Oct 08 08:20:17 2002 +0200
@@ -582,7 +582,6 @@
apply (unfold zcong_def dvd_def)
apply auto
apply (subgoal_tac "0 < m")
- apply (rotate_tac -1)
apply (simp add: int_0_le_mult_iff)
apply (subgoal_tac "m * k < m * 1")
apply (drule zmult_zless_cancel1 [THEN iffD1])
--- a/src/HOL/Subst/Unify.ML Mon Oct 07 19:01:51 2002 +0200
+++ b/src/HOL/Subst/Unify.ML Tue Oct 08 08:20:17 2002 +0200
@@ -215,7 +215,6 @@
(*Comb-Comb case*)
by (asm_simp_tac (simpset() addsplits [option.split]) 1);
by (strip_tac 1);
-by (rotate_tac ~2 1);
by (asm_full_simp_tac
(simpset() addsimps [MGUnifier_def, Unifier_def, MoreGeneral_def]) 1);
by (Safe_tac THEN rename_tac "theta sigma gamma" 1);