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