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/NumberTheory/Euler.thy
changeset 23373 ead82c82da9e
parent 22274 ce1459004c8d
child 25675 2488fc510178 
--- a/src/HOL/NumberTheory/Euler.thy	Wed Jun 13 16:43:02 2007 +0200
+++ b/src/HOL/NumberTheory/Euler.thy	Wed Jun 13 18:30:11 2007 +0200
@@ -264,7 +264,7 @@
     by (auto simp add: zEven_def zOdd_def)
   then have aux_1: "2 * ((p - 1) div 2) = (p - 1)"
     by (auto simp add: even_div_2_prop2)
-  then have "1 < (p - 1)"
+  with `2 < p` have "1 < (p - 1)"
     by auto
   then have " 1 < (2 * ((p - 1) div 2))"
     by (auto simp add: aux_1)
isabelle