# HG changeset patch
# User nipkow
# Date 1235292769 -3600
# Node ID 6cf1fe60ac7352e7299ac049426a46c733ec9505
# Parent 49f603f92c4726af753d07b808b3dafec916f010# Parent 46c88406e6c031aaaf76b970ef025894453de2ee
merged
diff -r 49f603f92c47 -r 6cf1fe60ac73 src/HOL/Extraction/Euclid.thy
--- a/src/HOL/Extraction/Euclid.thy Sat Feb 21 16:51:42 2009 -0800
+++ b/src/HOL/Extraction/Euclid.thy Sun Feb 22 09:52:49 2009 +0100
@@ -189,7 +189,7 @@
assume pn: "p \ 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