--- a/src/HOL/NumberTheory/Euler.thy Wed Mar 04 10:43:39 2009 +0100
+++ b/src/HOL/NumberTheory/Euler.thy Wed Mar 04 10:45:52 2009 +0100
@@ -272,7 +272,7 @@
text {* \medskip Prove the final part of Euler's Criterion: *}
lemma aux__1: "[| ~([x = 0] (mod p)); [y ^ 2 = x] (mod p)|] ==> ~(p dvd y)"
- by (metis dvdI power2_eq_square zcong_sym zcong_trans zcong_zero_equiv_div zdvd_trans)
+ by (metis dvdI power2_eq_square zcong_sym zcong_trans zcong_zero_equiv_div dvd_trans)
lemma aux__2: "2 * nat((p - 1) div 2) = nat (2 * ((p - 1) div 2))"
by (auto simp add: nat_mult_distrib)