# HG changeset patch # User wenzelm # Date 1224714271 -7200 # Node ID e79e196039a14933809fef2cfabfbdccb8673e30 # Parent 4adfdd666e7d032d092485535637caea58bcdbe5 fixed and reactivated HOL/Library/Pocklington.thy -- by Mark Hillebrand; diff -r 4adfdd666e7d -r e79e196039a1 src/HOL/Library/Library.thy --- 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 diff -r 4adfdd666e7d -r e79e196039a1 src/HOL/Library/Pocklington.thy --- 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 "\ = 0" by (simp add: mult_assoc mod_mult_self_is_0) + also have "\ = 0" by (simp add: mult_assoc) finally have False by simp } then have th11: "a ^ ((n - 1) div p) mod n \ 0" by auto have th1: "[a ^ ((n - 1) div p) mod n = a ^ ((n - 1) div p)] (mod n)"