summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
raw | gz |
help

author | nipkow |

Sun, 22 Feb 2009 09:52:28 +0100 | |

changeset 30047 | 46c88406e6c0 |

parent 30044 | f9182081d6c6 |

child 30048 | 6cf1fe60ac73 |

name fix

--- a/src/HOL/Extraction/Euclid.thy Sat Feb 21 21:00:50 2009 +0100 +++ b/src/HOL/Extraction/Euclid.thy Sun Feb 22 09:52:28 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