src/HOL/Number_Theory/Residues.thy
changeset 54489 03ff4d1e6784
parent 50027 7747a9f4c358
child 54611 31afce809794
     1.1 --- a/src/HOL/Number_Theory/Residues.thy	Tue Nov 19 01:30:14 2013 +0100
     1.2 +++ b/src/HOL/Number_Theory/Residues.thy	Tue Nov 19 10:05:53 2013 +0100
     1.3 @@ -455,6 +455,7 @@
     1.4    apply (subst fact_altdef_int, simp)
     1.5    apply (subst cong_int_def)
     1.6    apply simp
     1.7 +  apply arith
     1.8    apply (rule residues_prime.wilson_theorem1)
     1.9    apply (rule residues_prime.intro)
    1.10    apply auto