src/HOL/Old_Number_Theory/EulerFermat.thy
changeset 57514 bdc2c6b40bf2
parent 57418 6ab1c7cb0b8d
child 58889 5b7a9633cfa8
     1.1 --- a/src/HOL/Old_Number_Theory/EulerFermat.thy	Sat Jul 05 10:09:01 2014 +0200
     1.2 +++ b/src/HOL/Old_Number_Theory/EulerFermat.thy	Sat Jul 05 11:01:53 2014 +0200
     1.3 @@ -255,7 +255,7 @@
     1.4    apply (subst setprod.insert)
     1.5      apply (rule_tac [2] Bnor_prod_power_aux)
     1.6       apply (unfold inj_on_def)
     1.7 -     apply (simp_all add: mult_ac Bnor_fin Bnor_mem_zle_swap)
     1.8 +     apply (simp_all add: ac_simps Bnor_fin Bnor_mem_zle_swap)
     1.9    done
    1.10  
    1.11