# HG changeset patch
# User nipkow
# Date 1034058017 -7200
# Node ID a013a9dd370f4fe8d4c53b6792785a1251b3a41e
# Parent  a46362d2b19b6521c91099ebe9032c519bad8036
Got rid of rotates because of new simplifier

diff -r a46362d2b19b -r a013a9dd370f src/HOL/Auth/KerberosIV.ML
--- 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);
diff -r a46362d2b19b -r a013a9dd370f src/HOL/GroupTheory/Coset.thy
--- 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
 
diff -r a46362d2b19b -r a013a9dd370f src/HOL/GroupTheory/Sylow.thy
--- 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)
diff -r a46362d2b19b -r a013a9dd370f src/HOL/Hyperreal/HyperDef.ML
--- 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,
diff -r a46362d2b19b -r a013a9dd370f src/HOL/Hyperreal/Lim.ML
--- 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),  
diff -r a46362d2b19b -r a013a9dd370f src/HOL/IMP/Compiler.thy
--- 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
diff -r a46362d2b19b -r a013a9dd370f src/HOL/IMP/Hoare.thy
--- 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}"
diff -r a46362d2b19b -r a013a9dd370f src/HOL/MiniML/MiniML.ML
--- 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);
diff -r a46362d2b19b -r a013a9dd370f src/HOL/MiniML/Type.ML
--- 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);
diff -r a46362d2b19b -r a013a9dd370f src/HOL/NumberTheory/BijectionRel.thy
--- 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)
diff -r a46362d2b19b -r a013a9dd370f src/HOL/NumberTheory/IntPrimes.thy
--- 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])
diff -r a46362d2b19b -r a013a9dd370f src/HOL/Subst/Unify.ML
--- 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);