merged
authornipkow
Sun Feb 22 09:52:49 2009 +0100 (2009-02-22)
changeset 300486cf1fe60ac73
parent 30046 49f603f92c47
parent 30047 46c88406e6c0
child 30051 a416ed407f82
child 30052 410fefc247aa
merged
     1.1 --- a/src/HOL/Extraction/Euclid.thy	Sat Feb 21 16:51:42 2009 -0800
     1.2 +++ b/src/HOL/Extraction/Euclid.thy	Sun Feb 22 09:52:49 2009 +0100
     1.3 @@ -189,7 +189,7 @@
     1.4        assume pn: "p \<le> n"
     1.5        from `prime p` have "0 < p" by (rule prime_g_zero)
     1.6        then have "p dvd n!" using pn by (rule dvd_factorial)
     1.7 -      with dvd have "p dvd ?k - n!" by (rule dvd_diff)
     1.8 +      with dvd have "p dvd ?k - n!" by (rule nat_dvd_diff)
     1.9        then have "p dvd 1" by simp
    1.10        with prime show False using prime_nd_one by auto
    1.11      qed