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

author | wenzelm |

Thu, 23 Oct 2008 00:24:31 +0200 | |

changeset 28668 | e79e196039a1 |

parent 28667 | 4adfdd666e7d |

child 28669 | fdae33134bbf |

fixed and reactivated HOL/Library/Pocklington.thy -- by Mark Hillebrand;

src/HOL/Library/Library.thy | file | annotate | diff | comparison | revisions | |

src/HOL/Library/Pocklington.thy | file | annotate | diff | comparison | revisions |

--- a/src/HOL/Library/Library.thy Wed Oct 22 21:25:00 2008 +0200 +++ b/src/HOL/Library/Library.thy Thu Oct 23 00:24:31 2008 +0200 @@ -33,6 +33,7 @@ OptionalSugar Option_ord Permutation + Pocklington Primes Quicksort Quotient

--- a/src/HOL/Library/Pocklington.thy Wed Oct 22 21:25:00 2008 +0200 +++ b/src/HOL/Library/Pocklington.thy Thu Oct 23 00:24:31 2008 +0200 @@ -1273,7 +1273,7 @@ with eq0 have "a^ (n - 1) = (n*s)^p" by (simp add: power_mult[symmetric]) hence "1 = (n*s)^(Suc (p - 1)) mod n" using bqn p01 by simp - also have "\<dots> = 0" by (simp add: mult_assoc mod_mult_self_is_0) + also have "\<dots> = 0" by (simp add: mult_assoc) finally have False by simp } then have th11: "a ^ ((n - 1) div p) mod n \<noteq> 0" by auto have th1: "[a ^ ((n - 1) div p) mod n = a ^ ((n - 1) div p)] (mod n)"