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])