changeset 44766 | d4d33a4d7548 |
parent 40786 | 0a54cfc9add3 |
child 45480 | a39bb6d42ace |
--- a/src/HOL/Old_Number_Theory/EulerFermat.thy Tue Sep 06 16:30:39 2011 -0700 +++ b/src/HOL/Old_Number_Theory/EulerFermat.thy Tue Sep 06 19:03:41 2011 -0700 @@ -257,7 +257,7 @@ apply (subst setprod_insert) apply (rule_tac [2] Bnor_prod_power_aux) apply (unfold inj_on_def) - apply (simp_all add: zmult_ac Bnor_fin Bnor_mem_zle_swap) + apply (simp_all add: mult_ac Bnor_fin Bnor_mem_zle_swap) done