src/HOL/Old_Number_Theory/Euler.thy
 changeset 57514 bdc2c6b40bf2 parent 57512 cc97b347b301 child 58889 5b7a9633cfa8
```     1.1 --- a/src/HOL/Old_Number_Theory/Euler.thy	Sat Jul 05 10:09:01 2014 +0200
1.2 +++ b/src/HOL/Old_Number_Theory/Euler.thy	Sat Jul 05 11:01:53 2014 +0200
1.3 @@ -67,7 +67,7 @@
1.4    then have "[j * j = (a * MultInv p j) * j] (mod p)"
1.5      by (auto simp add: zcong_scalar)
1.6    then have a:"[j * j = a * (MultInv p j * j)] (mod p)"
1.7 -    by (auto simp add: mult_ac)
1.8 +    by (auto simp add: ac_simps)
1.9    have "[j * j = a] (mod p)"
1.10    proof -
1.11      from assms(1,2,4) have "[MultInv p j * j = 1] (mod p)"
1.12 @@ -149,7 +149,7 @@
1.13                     c = "a * (x * MultInv p x)" in  zcong_trans, force)
1.14    apply (frule_tac p = p and x = x in MultInv_prop2, auto)
1.15  apply (metis StandardRes_SRStar_prop3 mult_1_right mult.commute zcong_sym zcong_zmult_prop1)
1.16 -  apply (auto simp add: mult_ac)
1.17 +  apply (auto simp add: ac_simps)
1.18    done
1.19
1.20  lemma aux1: "[| 0 < x; (x::int) < a; x \<noteq> (a - 1) |] ==> x < a - 1"
```