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/Extraction/Euclid.thy
changeset 30240 5b25fee0362c
parent 27982 2aaa4a5569a6
child 31953 eeb8a300f362 
--- a/src/HOL/Extraction/Euclid.thy	Wed Mar 04 10:43:39 2009 +0100
+++ b/src/HOL/Extraction/Euclid.thy	Wed Mar 04 10:45:52 2009 +0100
@@ -189,7 +189,7 @@
       assume pn: "p \<le> n"
       from `prime p` have "0 < p" by (rule prime_g_zero)
       then have "p dvd n!" using pn by (rule dvd_factorial)
-      with dvd have "p dvd ?k - n!" by (rule dvd_diff)
+      with dvd have "p dvd ?k - n!" by (rule nat_dvd_diff)
       then have "p dvd 1" by simp
       with prime show False using prime_nd_one by auto
     qed
isabelle