src/HOL/Old_Number_Theory/WilsonRuss.thy
changeset 57512 cc97b347b301
parent 57418 6ab1c7cb0b8d
child 58889 5b7a9633cfa8
     1.1 --- a/src/HOL/Old_Number_Theory/WilsonRuss.thy	Fri Jul 04 20:07:08 2014 +0200
     1.2 +++ b/src/HOL/Old_Number_Theory/WilsonRuss.thy	Fri Jul 04 20:18:47 2014 +0200
     1.3 @@ -256,7 +256,7 @@
     1.4        apply (subgoal_tac [5]
     1.5          "zcong (a * inv p a * (\<Prod>x\<in>wset (a - 1) p. x)) (1 * 1) p")
     1.6         prefer 5
     1.7 -       apply (simp add: mult_assoc)
     1.8 +       apply (simp add: mult.assoc)
     1.9        apply (rule_tac [5] zcong_zmult)
    1.10         apply (rule_tac [5] inv_is_inv)
    1.11           apply (tactic "clarify_tac @{context} 4")