--- a/src/HOL/NumberTheory/WilsonRuss.thy Thu May 30 10:12:11 2002 +0200
+++ b/src/HOL/NumberTheory/WilsonRuss.thy Thu May 30 10:12:52 2002 +0200
@@ -344,7 +344,6 @@
apply safe
apply (rule_tac x = "2" in exI)
apply auto
- apply arith
done
theorem Wilson_Russ: