src/HOL/NumberTheory/WilsonRuss.thy
changeset 13187 e5434b822a96
parent 11868 56db9f3a6b3e
child 13524 604d0f3622d6
     1.1 --- a/src/HOL/NumberTheory/WilsonRuss.thy	Thu May 30 10:12:11 2002 +0200
     1.2 +++ b/src/HOL/NumberTheory/WilsonRuss.thy	Thu May 30 10:12:52 2002 +0200
     1.3 @@ -344,7 +344,6 @@
     1.4     apply safe
     1.5       apply (rule_tac x = "2" in exI)
     1.6       apply auto
     1.7 -  apply arith
     1.8    done
     1.9  
    1.10  theorem Wilson_Russ: