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