--- a/src/HOL/Old_Number_Theory/WilsonBij.thy Fri Jul 04 20:07:08 2014 +0200
+++ b/src/HOL/Old_Number_Theory/WilsonBij.thy Fri Jul 04 20:18:47 2014 +0200
@@ -207,7 +207,7 @@
lemma reciP_sym: "zprime p ==> symP (reciR p)"
apply (unfold reciR_def symP_def)
- apply (simp add: mult_commute)
+ apply (simp add: mult.commute)
apply auto
done
@@ -234,7 +234,7 @@
apply (subst setprod.insert)
apply (auto simp add: fin_bijER)
apply (subgoal_tac "zcong ((a * b) * \<Prod>A) (1 * 1) p")
- apply (simp add: mult_assoc)
+ apply (simp add: mult.assoc)
apply (rule zcong_zmult)
apply auto
done