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

--- 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)"