src/HOL/Number_Theory/Residues.thy
changeset 57514 bdc2c6b40bf2
parent 57512 cc97b347b301
child 58889 5b7a9633cfa8
     1.1 --- a/src/HOL/Number_Theory/Residues.thy	Sat Jul 05 10:09:01 2014 +0200
     1.2 +++ b/src/HOL/Number_Theory/Residues.thy	Sat Jul 05 11:01:53 2014 +0200
     1.3 @@ -40,7 +40,7 @@
     1.4    apply (insert m_gt_one)
     1.5    apply (rule abelian_groupI)
     1.6    apply (unfold R_def residue_ring_def)
     1.7 -  apply (auto simp add: mod_add_right_eq [symmetric] add_ac)
     1.8 +  apply (auto simp add: mod_add_right_eq [symmetric] ac_simps)
     1.9    apply (case_tac "x = 0")
    1.10    apply force
    1.11    apply (subgoal_tac "(x + (m - x)) mod m = 0")
    1.12 @@ -56,7 +56,7 @@
    1.13    apply (subgoal_tac "x * y mod m * z mod m = z * (x * y mod m) mod m")
    1.14    apply (erule ssubst)
    1.15    apply (subst mod_mult_right_eq [symmetric])+
    1.16 -  apply (simp_all only: mult_ac)
    1.17 +  apply (simp_all only: ac_simps)
    1.18    done
    1.19  
    1.20  lemma cring: "cring R"