src/HOL/Old_Number_Theory/Legacy_GCD.thy

           from H (3) have "a * ((b - 1) * y) + d * (b - 1 + 1) = d + x*b*(b - 1)" by algebra
           hence "a * ((b - 1) * y) = d + x*b*(b - 1) - d*b" using bp by simp
           hence "a * ((b - 1) * y) = d + (x*b*(b - 1) - d*b)" 
             by (simp only: diff_add_assoc[OF dble, of d, symmetric])
           hence "a * ((b - 1) * y) = b*(x*(b - 1) - d) + d"
-            by (simp only: diff_mult_distrib2 add.commute mult_ac)
+            by (simp only: diff_mult_distrib2 add.commute ac_simps)
           hence ?thesis using H(1,2)
             apply -
             apply (rule exI[where x=d], simp)
             apply (rule exI[where x="(b - 1) * y"])
             by (rule exI[where x="x*(b - 1) - d"], simp)}

   from assms obtain p where k_m: "k = m * p" using dvd_def by blast
   from assms obtain q where k_n: "k = n * q" using dvd_def by blast
   from pos_k k_m have pos_p: "p > 0" by auto
   from pos_k k_n have pos_q: "q > 0" by auto
   have "k * k * gcd q p = k * gcd (k * q) (k * p)"
-    by (simp add: mult_ac gcd_mult_distrib2)
+    by (simp add: ac_simps gcd_mult_distrib2)
   also have "\<dots> = k * gcd (m * p * q) (n * q * p)"
     by (simp add: k_m [symmetric] k_n [symmetric])
   also have "\<dots> = k * p * q * gcd m n"
-    by (simp add: mult_ac gcd_mult_distrib2)
+    by (simp add: ac_simps gcd_mult_distrib2)
   finally have "(m * p) * (n * q) * gcd q p = k * p * q * gcd m n"
     by (simp only: k_m [symmetric] k_n [symmetric])
   then have "p * q * m * n * gcd q p = p * q * k * gcd m n"
-    by (simp add: mult_ac)
+    by (simp add: ac_simps)
   with pos_p pos_q have "m * n * gcd q p = k * gcd m n"
     by simp
   with prod_gcd_lcm [of m n]
   have "lcm m n * gcd q p * gcd m n = k * gcd m n"
-    by (simp add: mult_ac)
+    by (simp add: ac_simps)
   with pos_gcd have "lcm m n * gcd q p = k" by simp
   then show ?thesis using dvd_def by auto
 qed
 
 lemma lcm_dvd1 [iff]:

   next
     case (Suc _)
     then have npos: "n > 0" by simp
     have "gcd m n dvd n" by simp
     then obtain k where "n = gcd m n * k" using dvd_def by auto
-    then have "m * n div gcd m n = m * (gcd m n * k) div gcd m n" by (simp add: mult_ac)
+    then have "m * n div gcd m n = m * (gcd m n * k) div gcd m n" by (simp add: ac_simps)
     also have "\<dots> = m * k" using mpos npos gcd_zero by simp
     finally show ?thesis by (simp add: lcm_def)
   qed
 qed
 

   next
     case (Suc _)
     then have mpos: "m > 0" by simp
     have "gcd m n dvd m" by simp
     then obtain k where "m = gcd m n * k" using dvd_def by auto
-    then have "m * n div gcd m n = (gcd m n * k) * n div gcd m n" by (simp add: mult_ac)
+    then have "m * n div gcd m n = (gcd m n * k) * n div gcd m n" by (simp add: ac_simps)
     also have "\<dots> = n * k" using mpos npos gcd_zero by simp
     finally show ?thesis by (simp add: lcm_def)
   qed
 qed