src/HOL/Number_Theory/Residues.thy
changeset 55172 92735f0d5302
parent 55161 8eb891539804
child 55227 653de351d21c
     1.1 --- a/src/HOL/Number_Theory/Residues.thy	Thu Jan 30 01:03:55 2014 +0100
     1.2 +++ b/src/HOL/Number_Theory/Residues.thy	Thu Jan 30 10:00:53 2014 +0100
     1.3 @@ -453,7 +453,6 @@
     1.4    apply (subst fact_altdef_int, simp)
     1.5    apply (subst cong_int_def)
     1.6    apply simp
     1.7 -  apply presburger
     1.8    apply (rule residues_prime.wilson_theorem1)
     1.9    apply (rule residues_prime.intro)
    1.10    apply auto