src/HOL/Power.thy
changeset 57514 bdc2c6b40bf2
parent 57512 cc97b347b301
child 58157 c376c43c346c
     1.1 --- a/src/HOL/Power.thy	Sat Jul 05 10:09:01 2014 +0200
     1.2 +++ b/src/HOL/Power.thy	Sat Jul 05 11:01:53 2014 +0200
     1.3 @@ -110,7 +110,7 @@
     1.4  
     1.5  lemma power_mult_distrib [field_simps]:
     1.6    "(a * b) ^ n = (a ^ n) * (b ^ n)"
     1.7 -  by (induct n) (simp_all add: mult_ac)
     1.8 +  by (induct n) (simp_all add: ac_simps)
     1.9  
    1.10  end
    1.11  
    1.12 @@ -562,7 +562,7 @@
    1.13  next
    1.14    case (Suc n)
    1.15    have "a ^ Suc (2 * Suc n) = (a*a) * a ^ Suc(2*n)"
    1.16 -    by (simp add: mult_ac power_add power2_eq_square)
    1.17 +    by (simp add: ac_simps power_add power2_eq_square)
    1.18    thus ?case
    1.19      by (simp del: power_Suc add: Suc mult_less_0_iff mult_neg_neg)
    1.20  qed
    1.21 @@ -580,7 +580,7 @@
    1.22  next
    1.23    case (Suc n)
    1.24      have "a ^ (2 * Suc n) = (a*a) * a ^ (2*n)" 
    1.25 -      by (simp add: mult_ac power_add power2_eq_square)
    1.26 +      by (simp add: ac_simps power_add power2_eq_square)
    1.27      thus ?case
    1.28        by (simp add: Suc zero_le_mult_iff)
    1.29  qed