src/HOL/Number_Theory/Residues.thy
changeset 57512 cc97b347b301
parent 55352 1d2852dfc4a7
child 57514 bdc2c6b40bf2
     1.1 --- a/src/HOL/Number_Theory/Residues.thy	Fri Jul 04 20:07:08 2014 +0200
     1.2 +++ b/src/HOL/Number_Theory/Residues.thy	Fri Jul 04 20:18:47 2014 +0200
     1.3 @@ -65,7 +65,7 @@
     1.4    apply (rule comm_monoid)
     1.5    apply (unfold R_def residue_ring_def, auto)
     1.6    apply (subst mod_add_eq [symmetric])
     1.7 -  apply (subst mult_commute)
     1.8 +  apply (subst mult.commute)
     1.9    apply (subst mod_mult_right_eq [symmetric])
    1.10    apply (simp add: field_simps)
    1.11    done
    1.12 @@ -105,7 +105,7 @@
    1.13    apply auto
    1.14    apply (metis invertible_coprime_int)
    1.15    apply (subst (asm) coprime_iff_invertible'_int)
    1.16 -  apply (auto simp add: cong_int_def mult_commute)
    1.17 +  apply (auto simp add: cong_int_def mult.commute)
    1.18    done
    1.19  
    1.20  lemma res_neg_eq: "\<ominus> x = (- x) mod m"
    1.21 @@ -120,7 +120,7 @@
    1.22    apply auto
    1.23    apply (subgoal_tac "y mod m = - x mod m")
    1.24    apply simp
    1.25 -  apply (metis minus_add_cancel mod_mult_self1 mult_commute)
    1.26 +  apply (metis minus_add_cancel mod_mult_self1 mult.commute)
    1.27    done
    1.28  
    1.29  lemma finite [iff]: "finite (carrier R)"
    1.30 @@ -159,7 +159,7 @@
    1.31    apply (insert m_gt_one)
    1.32    apply (induct n)
    1.33    apply (auto simp add: nat_pow_def one_cong)
    1.34 -  apply (metis mult_commute mult_cong)
    1.35 +  apply (metis mult.commute mult_cong)
    1.36    done
    1.37  
    1.38  lemma neg_cong: "\<ominus> (x mod m) = (- x) mod m"
    1.39 @@ -196,7 +196,7 @@
    1.40  
    1.41  lemma one_eq_neg_one: "\<one> = \<ominus> \<one> \<Longrightarrow> m = 2"
    1.42    apply (simp add: res_one_eq res_neg_eq)
    1.43 -  apply (metis add_commute add_diff_cancel mod_mod_trivial one_add_one uminus_add_conv_diff
    1.44 +  apply (metis add.commute add_diff_cancel mod_mod_trivial one_add_one uminus_add_conv_diff
    1.45              zero_neq_one zmod_zminus1_eq_if)
    1.46    done
    1.47