# HG changeset patch # User wenzelm # Date 1246990566 -7200 # Node ID eeb8a300f362313c029b903101cb6147e7fee87a # Parent 40501bb2d57ccceac97c35919ad89c6e24c369da fixed proof (cf. 40501bb2d57c); diff -r 40501bb2d57c -r eeb8a300f362 src/HOL/Extraction/Euclid.thy --- a/src/HOL/Extraction/Euclid.thy Tue Jul 07 17:39:51 2009 +0200 +++ b/src/HOL/Extraction/Euclid.thy Tue Jul 07 20:16:06 2009 +0200 @@ -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 nat_dvd_diff) + with dvd have "p dvd ?k - n!" by (rule dvd_diff_nat) then have "p dvd 1" by simp with prime show False using prime_nd_one by auto qed