src/HOL/Number_Theory/Gauss.thy
changeset 58645 94bef115c08f
parent 58410 6d46ad54a2ab
child 58834 773b378d9313
     1.1 --- a/src/HOL/Number_Theory/Gauss.thy	Fri Oct 10 18:23:59 2014 +0200
     1.2 +++ b/src/HOL/Number_Theory/Gauss.thy	Thu Oct 09 22:43:48 2014 +0200
     1.3 @@ -57,7 +57,7 @@
     1.4  
     1.5  lemma p_odd_int: obtains z::int where "int p = 2*z+1" "0<z"
     1.6    using odd_p p_ge_2
     1.7 -  by (auto simp add: even_def) (metis p_eq2)
     1.8 +  by (auto simp add: even_iff_mod_2_eq_zero) (metis p_eq2)
     1.9  
    1.10  
    1.11  subsection {* Basic Properties of the Gauss Sets *}