--- a/src/HOL/Old_Number_Theory/Gauss.thy Tue Sep 06 16:30:39 2011 -0700
+++ b/src/HOL/Old_Number_Theory/Gauss.thy Tue Sep 06 19:03:41 2011 -0700
@@ -344,7 +344,7 @@
apply (elim zcong_trans)
by (simp only: zcong_refl)
also have "y * a + ya * a = a * (y + ya)"
- by (simp add: zadd_zmult_distrib2 zmult_commute)
+ by (simp add: right_distrib mult_commute)
finally have "[a * (y + ya) = 0] (mod p)" .
with p_prime a_nonzero zcong_zprime_prod_zero [of p a "y + ya"]
p_a_relprime
@@ -429,7 +429,7 @@
also have "setprod uminus E = (setprod id E) * (-1)^(card E)"
using finite_E by (induct set: finite) auto
then have "setprod uminus E = (-1) ^ (card E) * (setprod id E)"
- by (simp add: zmult_commute)
+ by (simp add: mult_commute)
with two show ?thesis
by simp
qed
@@ -444,7 +444,7 @@
"[a ^ nat((p - 1) div 2) = (-1) ^ (card E)] (mod p)"
proof -
have "[setprod id A = setprod id F * setprod id D](mod p)"
- by (auto simp add: prod_D_F_eq_prod_A zmult_commute cong del:setprod_cong)
+ by (auto simp add: prod_D_F_eq_prod_A mult_commute cong del:setprod_cong)
then have "[setprod id A = ((-1)^(card E) * setprod id E) *
setprod id D] (mod p)"
apply (rule zcong_trans)
@@ -453,7 +453,7 @@
then have "[setprod id A = ((-1)^(card E) * setprod id C)] (mod p)"
apply (rule zcong_trans)
apply (insert C_prod_eq_D_times_E, erule subst)
- apply (subst zmult_assoc, auto)
+ apply (subst mult_assoc, auto)
done
then have "[setprod id A = ((-1)^(card E) * setprod id B)] (mod p)"
apply (rule zcong_trans)
@@ -474,7 +474,7 @@
then have "[setprod id A = ((-1)^(card E) * a^(card A) *
setprod id A)](mod p)"
apply (rule zcong_trans)
- apply (simp add: zcong_scalar2 zcong_scalar finite_A setprod_constant zmult_assoc)
+ apply (simp add: zcong_scalar2 zcong_scalar finite_A setprod_constant mult_assoc)
done
then have a: "[setprod id A * (-1)^(card E) =
((-1)^(card E) * a^(card A) * setprod id A * (-1)^(card E))](mod p)"