Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/Number_Theory/Gauss.thy
changeset 58834 773b378d9313
parent 58645 94bef115c08f
child 58889 5b7a9633cfa8 
--- a/src/HOL/Number_Theory/Gauss.thy	Thu Oct 30 16:36:44 2014 +0000
+++ b/src/HOL/Number_Theory/Gauss.thy	Thu Oct 30 21:02:01 2014 +0100
@@ -53,7 +53,7 @@
 
 lemma p_eq2: "int p = (2 * ((int p - 1) div 2)) + 1"
   using odd_p p_ge_2 div_mult_self1_is_id [of 2 "p - 1"]   
-  by auto presburger
+  by simp
 
 lemma p_odd_int: obtains z::int where "int p = 2*z+1" "0<z"
   using odd_p p_ge_2
isabelle