# HG changeset patch
# User wenzelm
# Date 1160353191 -7200
# Node ID 113c9516a2d76c9c7c96a41aa119fbc390101d6b
# Parent  3f8d2834b2c49f6cd856e31003c43cfa90e1dbaf
attribute symmetric: zero_var_indexes;

diff -r 3f8d2834b2c4 -r 113c9516a2d7 src/HOL/Hyperreal/HSeries.thy
--- a/src/HOL/Hyperreal/HSeries.thy	Mon Oct 09 02:19:49 2006 +0200
+++ b/src/HOL/Hyperreal/HSeries.thy	Mon Oct 09 02:19:51 2006 +0200
@@ -83,7 +83,7 @@
 done
 
 lemma sumhr_split_diff: "n<p ==> sumhr(0,p,f) - sumhr(0,n,f) = sumhr(n,p,f)"
-by (drule_tac f1 = f in sumhr_split_add [symmetric], simp)
+by (drule_tac f = f in sumhr_split_add [symmetric], simp)
 
 lemma sumhr_hrabs: "abs(sumhr(m,n,f)) \<le> sumhr(m,n,%i. abs(f i))"
 apply (cases n, cases m)
diff -r 3f8d2834b2c4 -r 113c9516a2d7 src/HOL/Hyperreal/HTranscendental.thy
--- a/src/HOL/Hyperreal/HTranscendental.thy	Mon Oct 09 02:19:49 2006 +0200
+++ b/src/HOL/Hyperreal/HTranscendental.thy	Mon Oct 09 02:19:51 2006 +0200
@@ -71,7 +71,7 @@
 
 lemma hypreal_inverse_sqrt_pow2:
      "0 < x ==> inverse (( *f* sqrt)(x)) ^ 2 = inverse x"
-apply (cut_tac n1 = 2 and a1 = "( *f* sqrt) x" in power_inverse [symmetric])
+apply (cut_tac n = 2 and a = "( *f* sqrt) x" in power_inverse [symmetric])
 apply (auto dest: hypreal_sqrt_gt_zero_pow2)
 done
 
diff -r 3f8d2834b2c4 -r 113c9516a2d7 src/HOL/Hyperreal/NthRoot.thy
--- a/src/HOL/Hyperreal/NthRoot.thy	Mon Oct 09 02:19:49 2006 +0200
+++ b/src/HOL/Hyperreal/NthRoot.thy	Mon Oct 09 02:19:51 2006 +0200
@@ -358,7 +358,7 @@
 done
 
 lemma real_inv_sqrt_pow2: "0 < x ==> inverse (sqrt(x)) ^ 2 = inverse x"
-by (cut_tac n1 = 2 and a1 = "sqrt x" in power_inverse [symmetric], auto)
+by (cut_tac n = 2 and a = "sqrt x" in power_inverse [symmetric], auto)
 
 lemma real_sqrt_eq_zero_cancel: "[| 0 \<le> x; sqrt(x) = 0|] ==> x = 0"
 apply (drule real_le_imp_less_or_eq)
diff -r 3f8d2834b2c4 -r 113c9516a2d7 src/HOL/Hyperreal/Poly.thy
--- a/src/HOL/Hyperreal/Poly.thy	Mon Oct 09 02:19:49 2006 +0200
+++ b/src/HOL/Hyperreal/Poly.thy	Mon Oct 09 02:19:51 2006 +0200
@@ -964,7 +964,7 @@
 apply (simp add: rsquarefree_def, safe)
 apply (frule_tac a = a in order_decomp)
 apply (drule_tac x = a in spec)
-apply (drule_tac a1 = a in order_root2 [symmetric])
+apply (drule_tac a = a in order_root2 [symmetric])
 apply (auto simp del: pmult_Cons)
 apply (rule_tac x = q in exI, safe)
 apply (simp add: poly_mult fun_eq)
diff -r 3f8d2834b2c4 -r 113c9516a2d7 src/HOL/NumberTheory/Gauss.thy
--- a/src/HOL/NumberTheory/Gauss.thy	Mon Oct 09 02:19:49 2006 +0200
+++ b/src/HOL/NumberTheory/Gauss.thy	Mon Oct 09 02:19:51 2006 +0200
@@ -308,7 +308,7 @@
 lemma (in GAUSS) C_B_zcong_prod: "[setprod id C = setprod id B] (mod p)"
   apply (auto simp add: C_def)
   apply (insert finite_B SR_B_inj)
-  apply (frule_tac f1 = "StandardRes p" in setprod_reindex_id [symmetric], auto)
+  apply (frule_tac f = "StandardRes p" in setprod_reindex_id [symmetric], auto)
   apply (rule setprod_same_function_zcong)
   apply (auto simp add: StandardRes_prop1 zcong_sym p_g_0)
   done
diff -r 3f8d2834b2c4 -r 113c9516a2d7 src/HOL/NumberTheory/Quadratic_Reciprocity.thy
--- a/src/HOL/NumberTheory/Quadratic_Reciprocity.thy	Mon Oct 09 02:19:49 2006 +0200
+++ b/src/HOL/NumberTheory/Quadratic_Reciprocity.thy	Mon Oct 09 02:19:51 2006 +0200
@@ -604,7 +604,7 @@
       nat(setsum (%x. ((x * q) div p)) P_set) =
         nat((setsum (%x. ((x * p) div q)) Q_set) +
           (setsum (%x. ((x * q) div p)) P_set))"
-    apply (rule_tac z1 = "setsum (%x. ((x * p) div q)) Q_set" in
+    apply (rule_tac z = "setsum (%x. ((x * p) div q)) Q_set" in
       nat_add_distrib [symmetric])
     apply (auto simp add: S1_carda [symmetric] S2_carda [symmetric])
     done
diff -r 3f8d2834b2c4 -r 113c9516a2d7 src/Pure/Isar/calculation.ML
--- a/src/Pure/Isar/calculation.ML	Mon Oct 09 02:19:49 2006 +0200
+++ b/src/Pure/Isar/calculation.ML	Mon Oct 09 02:19:51 2006 +0200
@@ -85,7 +85,7 @@
 
 val symmetric = Thm.rule_attribute (fn x => fn th =>
   (case Seq.chop 2 (Drule.multi_resolves [th] (#2 (#1 (CalculationData.get x)))) of
-    ([th'], _) => th'
+    ([th'], _) => Drule.zero_var_indexes th'
   | ([], _) => raise THM ("symmetric: no unifiers", 1, [th])
   | _ => raise THM ("symmetric: multiple unifiers", 1, [th])));
 
diff -r 3f8d2834b2c4 -r 113c9516a2d7 src/ZF/Induct/Multiset.thy
--- a/src/ZF/Induct/Multiset.thy	Mon Oct 09 02:19:49 2006 +0200
+++ b/src/ZF/Induct/Multiset.thy	Mon Oct 09 02:19:51 2006 +0200
@@ -637,8 +637,8 @@
   shows "P(M)"
 apply (rule multiset_induct2 [OF M])
 apply (simp_all add: P0)
-apply (frule_tac [2] a1 = b in munion_single_case2 [symmetric])
-apply (frule_tac a1 = a in munion_single_case1 [symmetric])
+apply (frule_tac [2] a = b in munion_single_case2 [symmetric])
+apply (frule_tac a = a in munion_single_case1 [symmetric])
 apply (auto intro: step)
 done