1.1 --- a/src/HOL/Auth/KerberosIV.ML	Mon Oct 07 19:01:51 2002 +0200
     1.2 +++ b/src/HOL/Auth/KerberosIV.ML	Tue Oct 08 08:20:17 2002 +0200
     1.3 @@ -772,7 +772,6 @@
     1.4    conclude AuthKey \\<noteq> AuthKeya.*)
     1.5  by (Clarify_tac 9);
     1.6  by analz_sees_tac;
     1.7 -by (rotate_tac ~1 11);
     1.8  by (ALLGOALS 
     1.9      (asm_full_simp_tac 
    1.10       (simpset() addsimps [less_SucI, new_keys_not_analzd,
    1.11 @@ -800,7 +799,6 @@
    1.12  by (thin_tac "Says Aa Tgs ?X \\<in> set ?evs" 1);
    1.13  by (forward_tac [Says_imp_spies RS parts.Inj RS ServKey_notin_AuthKeysD] 1);
    1.14  by (assume_tac 1 THEN Blast_tac 1 THEN assume_tac 1);
    1.15 -by (rotate_tac ~1 1);
    1.16  by (asm_full_simp_tac (simpset() addsimps [analz_insert_freshK2]) 1);
    1.17  by (blast_tac (claset() addDs [Says_imp_spies RS parts.Inj, Key_unique_SesKey] 
    1.18                          addIs  [less_SucI]) 1);

     2.1 --- a/src/HOL/GroupTheory/Coset.thy	Mon Oct 07 19:01:51 2002 +0200
     2.2 +++ b/src/HOL/GroupTheory/Coset.thy	Tue Oct 08 08:20:17 2002 +0200
     2.3 @@ -345,7 +345,6 @@
     2.4  apply (rule inj_onI)
     2.5  apply (subgoal_tac "x \<in> carrier G & y \<in> carrier G")
     2.6   prefer 2 apply (blast intro: r_coset_subset_G [THEN subsetD])
     2.7 -apply (rotate_tac -1)
     2.8  apply (simp add: subsetD)
     2.9  done
    2.10  

     3.1 --- a/src/HOL/GroupTheory/Sylow.thy	Mon Oct 07 19:01:51 2002 +0200
     3.2 +++ b/src/HOL/GroupTheory/Sylow.thy	Tue Oct 08 08:20:17 2002 +0200
     3.3 @@ -289,7 +289,7 @@
     3.4  apply (rule bexI)
     3.5  apply (rule_tac [2] setrcos_H_funcset_M)
     3.6  apply (rule inj_onI)
     3.7 -apply (rotate_tac -2, simp)
     3.8 +apply (simp)
     3.9  apply (rule trans [OF _ H_elem_map_eq])
    3.10  prefer 2 apply assumption
    3.11  apply (rule H_elem_map_eq [symmetric, THEN trans], assumption)

     4.1 --- a/src/HOL/Hyperreal/HyperDef.ML	Mon Oct 07 19:01:51 2002 +0200
     4.2 +++ b/src/HOL/Hyperreal/HyperDef.ML	Tue Oct 08 08:20:17 2002 +0200
     4.3 @@ -119,12 +119,11 @@
     4.4  
     4.5  Goal "{n::nat. P} : FreeUltrafilterNat ==> P";
     4.6  by (rtac ccontr 1);
     4.7 -by (rotate_tac 1 1);
     4.8  by (Asm_full_simp_tac 1);
     4.9  qed "FreeUltrafilterNat_P";
    4.10  
    4.11  Goal "{n. P(n)} : FreeUltrafilterNat ==> EX n. P(n)";
    4.12 -by (rtac ccontr 1 THEN rotate_tac 1 1);
    4.13 +by (rtac ccontr 1);
    4.14  by (Asm_full_simp_tac 1);
    4.15  qed "FreeUltrafilterNat_Ex_P";
    4.16  
    4.17 @@ -262,7 +261,7 @@
    4.18  by (dtac eq_equiv_class 1);
    4.19  by (rtac equiv_hyprel 1);
    4.20  by (Fast_tac 1);
    4.21 -by (rtac ccontr 1 THEN rotate_tac 1 1);
    4.22 +by (rtac ccontr 1);
    4.23  by Auto_tac;
    4.24  qed "inj_hypreal_of_real";
    4.25  
    4.26 @@ -631,7 +630,6 @@
    4.27  Goalw [hypreal_one_def,hypreal_zero_def] 
    4.28       "x ~= 0 ==> x*inverse(x) = (1::hypreal)";
    4.29  by (res_inst_tac [("z","x")] eq_Abs_hypreal 1);
    4.30 -by (rotate_tac 1 1);
    4.31  by (asm_full_simp_tac (simpset() addsimps [hypreal_inverse, hypreal_mult]) 1);
    4.32  by (dtac FreeUltrafilterNat_Compl_mem 1);
    4.33  by (blast_tac (claset() addSIs [real_mult_inv_right,

     5.1 --- a/src/HOL/Hyperreal/Lim.ML	Mon Oct 07 19:01:51 2002 +0200
     5.2 +++ b/src/HOL/Hyperreal/Lim.ML	Tue Oct 08 08:20:17 2002 +0200
     5.3 @@ -877,7 +877,6 @@
     5.4       approx_mult1 1);
     5.5  by (ALLGOALS(dtac (hypreal_not_eq_minus_iff RS iffD1)));
     5.6  by (subgoal_tac "(*f* (%z. z - x)) u \\<noteq> (0::hypreal)" 2);
     5.7 -by (rotate_tac ~1 2);
     5.8  by (auto_tac (claset(),
     5.9      simpset() addsimps [real_diff_def, hypreal_diff_def, 
    5.10  		(approx_minus_iff RS iffD1) RS (mem_infmal_iff RS iffD2),  

     6.1 --- a/src/HOL/IMP/Compiler.thy	Mon Oct 07 19:01:51 2002 +0200
     6.2 +++ b/src/HOL/IMP/Compiler.thy	Tue Oct 08 08:20:17 2002 +0200
     6.3 @@ -97,10 +97,8 @@
     6.4  apply(rule iffI)
     6.5   defer apply simp
     6.6  apply(subgoal_tac "n \<le> size p1")
     6.7 - apply(rotate_tac -1)
     6.8   apply simp
     6.9  apply(rule ccontr)
    6.10 -apply(rotate_tac -1)
    6.11  apply(drule_tac f = length in arg_cong)
    6.12  apply simp
    6.13  apply arith

     7.1 --- a/src/HOL/IMP/Hoare.thy	Mon Oct 07 19:01:51 2002 +0200
     7.2 +++ b/src/HOL/IMP/Hoare.thy	Tue Oct 08 08:20:17 2002 +0200
     7.3 @@ -116,9 +116,7 @@
     7.4   apply (rule weak_coinduct)
     7.5    apply (erule CollectI)
     7.6   apply safe
     7.7 -  apply (rotate_tac -1)
     7.8    apply simp
     7.9 - apply (rotate_tac -1)
    7.10   apply simp
    7.11  apply (simp add: wp_def Gamma_def)
    7.12  apply (intro strip)
    7.13 @@ -146,8 +144,8 @@
    7.14   apply (rule hoare_conseq1)
    7.15    prefer 2 apply (fast)
    7.16    apply safe
    7.17 - apply (rotate_tac -1, simp)
    7.18 -apply (rotate_tac -1, simp)
    7.19 + apply simp
    7.20 +apply simp
    7.21  done
    7.22  
    7.23  lemma hoare_relative_complete: "|= {P}c{Q} ==> |- {P}c{Q}"

     8.1 --- a/src/HOL/MiniML/MiniML.ML	Mon Oct 07 19:01:51 2002 +0200
     8.2 +++ b/src/HOL/MiniML/MiniML.ML	Tue Oct 08 08:20:17 2002 +0200
     8.3 @@ -90,7 +90,6 @@
     8.4  by (rtac ballI 1);
     8.5  by (etac UN_E 1);
     8.6  by (dtac (dom_S' RS subsetD) 1);
     8.7 -by (rotate_tac 1 1);
     8.8  by (Asm_full_simp_tac 1);
     8.9  by (fast_tac (claset() addDs [free_tv_of_substitutions_extend_to_scheme_lists] 
    8.10                        addIs [free_tv_of_substitutions_extend_to_types RS subsetD]) 1);

     9.1 --- a/src/HOL/MiniML/Type.ML	Mon Oct 07 19:01:51 2002 +0200
     9.2 +++ b/src/HOL/MiniML/Type.ML	Tue Oct 08 08:20:17 2002 +0200
     9.3 @@ -269,7 +269,6 @@
     9.4  by (Simp_tac 1);
     9.5  by (safe_tac (empty_cs addSIs [exI,conjI,notI]));
     9.6  by (assume_tac 2);
     9.7 -by (rotate_tac 1 1);
     9.8  by (Asm_full_simp_tac 1);
     9.9  qed "cod_app_subst";
    9.10  Addsimps [cod_app_subst];
    9.11 @@ -474,7 +473,6 @@
    9.12  by (simp_tac (simpset() addsimps [free_tv_subst,dom_def,cod_def]) 1);
    9.13  by (strip_tac 1);
    9.14  by (case_tac "S nat = TVar nat" 1);
    9.15 -by (rotate_tac 3 1);
    9.16  by (Asm_full_simp_tac 1);
    9.17  by (dres_inst_tac [("x","m")] spec 1);
    9.18  by (Fast_tac 1);

    10.1 --- a/src/HOL/NumberTheory/BijectionRel.thy	Mon Oct 07 19:01:51 2002 +0200
    10.2 +++ b/src/HOL/NumberTheory/BijectionRel.thy	Tue Oct 08 08:20:17 2002 +0200
    10.3 @@ -191,7 +191,6 @@
    10.4     apply clarify
    10.5     apply (case_tac "b \<in> F")
    10.6      prefer 2
    10.7 -    apply (rotate_tac -1)
    10.8      apply (simp add: subset_insert)
    10.9     apply (cut_tac F = F and a = b and A = A and B = B in aux1)
   10.10          prefer 6
   10.11 @@ -205,7 +204,6 @@
   10.12    apply clarify
   10.13    apply (case_tac "a \<in> F")
   10.14     apply (case_tac [!] "b \<in> F")
   10.15 -     apply (rotate_tac [2-4] -2)
   10.16       apply (cut_tac F = F and a = a and b = b and A = A and B = B
   10.17         in aux2)
   10.18              apply (simp_all add: subset_insert)

    11.1 --- a/src/HOL/NumberTheory/IntPrimes.thy	Mon Oct 07 19:01:51 2002 +0200
    11.2 +++ b/src/HOL/NumberTheory/IntPrimes.thy	Tue Oct 08 08:20:17 2002 +0200
    11.3 @@ -582,7 +582,6 @@
    11.4    apply (unfold zcong_def dvd_def)
    11.5    apply auto
    11.6    apply (subgoal_tac "0 < m")
    11.7 -   apply (rotate_tac -1)
    11.8     apply (simp add: int_0_le_mult_iff)
    11.9     apply (subgoal_tac "m * k < m * 1")
   11.10      apply (drule zmult_zless_cancel1 [THEN iffD1])

    12.1 --- a/src/HOL/Subst/Unify.ML	Mon Oct 07 19:01:51 2002 +0200
    12.2 +++ b/src/HOL/Subst/Unify.ML	Tue Oct 08 08:20:17 2002 +0200
    12.3 @@ -215,7 +215,6 @@
    12.4  (*Comb-Comb case*)
    12.5  by (asm_simp_tac (simpset() addsplits [option.split]) 1);
    12.6  by (strip_tac 1);
    12.7 -by (rotate_tac ~2 1);
    12.8  by (asm_full_simp_tac 
    12.9      (simpset() addsimps [MGUnifier_def, Unifier_def, MoreGeneral_def]) 1);
   12.10  by (Safe_tac THEN rename_tac "theta sigma gamma" 1);