src/HOL/Old_Number_Theory/Euler.thy
changeset 57512 cc97b347b301
parent 57492 74bf65a1910a
child 57514 bdc2c6b40bf2
     1.1 --- a/src/HOL/Old_Number_Theory/Euler.thy	Fri Jul 04 20:07:08 2014 +0200
     1.2 +++ b/src/HOL/Old_Number_Theory/Euler.thy	Fri Jul 04 20:18:47 2014 +0200
     1.3 @@ -148,7 +148,7 @@
     1.4                     b = "x * (a * MultInv p x)" and
     1.5                     c = "a * (x * MultInv p x)" in  zcong_trans, force)
     1.6    apply (frule_tac p = p and x = x in MultInv_prop2, auto)
     1.7 -apply (metis StandardRes_SRStar_prop3 mult_1_right mult_commute zcong_sym zcong_zmult_prop1)
     1.8 +apply (metis StandardRes_SRStar_prop3 mult_1_right mult.commute zcong_sym zcong_zmult_prop1)
     1.9    apply (auto simp add: mult_ac)
    1.10    done
    1.11