src/HOL/Library/Fundamental_Theorem_Algebra.thy
changeset 57514 bdc2c6b40bf2
parent 57512 cc97b347b301
child 57862 8f074e6e22fc
     1.1 --- a/src/HOL/Library/Fundamental_Theorem_Algebra.thy	Sat Jul 05 10:09:01 2014 +0200
     1.2 +++ b/src/HOL/Library/Fundamental_Theorem_Algebra.thy	Sat Jul 05 11:01:53 2014 +0200
     1.3 @@ -732,7 +732,7 @@
     1.4      {
     1.5        fix w
     1.6        have "cmod (poly ?r w) < 1 \<longleftrightarrow> cmod (poly q w / ?a0) < 1"
     1.7 -        using qr[rule_format, of w] a00 by (simp add: divide_inverse mult_ac)
     1.8 +        using qr[rule_format, of w] a00 by (simp add: divide_inverse ac_simps)
     1.9        also have "\<dots> \<longleftrightarrow> cmod (poly q w) < cmod ?a0"
    1.10          using a00 unfolding norm_divide by (simp add: field_simps)
    1.11        finally have "cmod (poly ?r w) < 1 \<longleftrightarrow> cmod (poly q w) < cmod ?a0" .
    1.12 @@ -980,7 +980,7 @@
    1.13                  have "p = [:- a, 1:] ^ (Suc ?op) * u"
    1.14                    apply (subst s)
    1.15                    apply (subst u)
    1.16 -                  apply (simp only: power_Suc mult_ac)
    1.17 +                  apply (simp only: power_Suc ac_simps)
    1.18                    done
    1.19                  with ap(2)[unfolded dvd_def] have False
    1.20                    by blast
    1.21 @@ -1010,7 +1010,7 @@
    1.22                apply (subst mult.assoc [where a=u])
    1.23                apply (subst mult.assoc [where b=u, symmetric])
    1.24                apply (subst u [symmetric])
    1.25 -              apply (simp add: mult_ac power_add [symmetric])
    1.26 +              apply (simp add: ac_simps power_add [symmetric])
    1.27                done
    1.28              then have ?ths
    1.29                unfolding dvd_def by blast