changeset 57418 | 6ab1c7cb0b8d |
parent 46008 | c296c75f4cf4 |
child 57514 | bdc2c6b40bf2 |
--- a/src/HOL/Old_Number_Theory/EulerFermat.thy Fri Jun 27 22:08:55 2014 +0200 +++ b/src/HOL/Old_Number_Theory/EulerFermat.thy Sat Jun 28 09:16:42 2014 +0200 @@ -252,7 +252,7 @@ apply (simplesubst BnorRset.simps) --{*multiple redexes*} apply (unfold Let_def, auto) apply (simp add: Bnor_fin Bnor_mem_zle_swap) - apply (subst setprod_insert) + apply (subst setprod.insert) apply (rule_tac [2] Bnor_prod_power_aux) apply (unfold inj_on_def) apply (simp_all add: mult_ac Bnor_fin Bnor_mem_zle_swap)