changeset 30042 | 31039ee583fa |
parent 27556 | 292098f2efdf |
--- a/src/HOL/NumberTheory/EulerFermat.thy Sat Feb 21 09:58:45 2009 +0100 +++ b/src/HOL/NumberTheory/EulerFermat.thy Sat Feb 21 20:52:30 2009 +0100 @@ -155,7 +155,7 @@ prefer 2 apply (subst zdvd_iff_zgcd [symmetric]) apply (rule_tac [4] zgcd_zcong_zgcd) - apply (simp_all add: zdvd_zminus_iff zcong_sym) + apply (simp_all add: zcong_sym) done