1.1 --- a/src/HOL/Number_Theory/Gauss.thy	Thu Oct 30 16:36:44 2014 +0000
     1.2 +++ b/src/HOL/Number_Theory/Gauss.thy	Thu Oct 30 21:02:01 2014 +0100
     1.3 @@ -53,7 +53,7 @@
     1.4  
     1.5  lemma p_eq2: "int p = (2 * ((int p - 1) div 2)) + 1"
     1.6    using odd_p p_ge_2 div_mult_self1_is_id [of 2 "p - 1"]   
     1.7 -  by auto presburger
     1.8 +  by simp
     1.9  
    1.10  lemma p_odd_int: obtains z::int where "int p = 2*z+1" "0<z"
    1.11    using odd_p p_ge_2