src/HOL/Library/Fundamental_Theorem_Algebra.thy
 changeset 37887 2ae085b07f2f parent 37093 8808a1aa12a2 child 41529 ba60efa2fd08
```     1.1 --- a/src/HOL/Library/Fundamental_Theorem_Algebra.thy	Mon Jul 19 16:09:44 2010 +0200
1.2 +++ b/src/HOL/Library/Fundamental_Theorem_Algebra.thy	Mon Jul 19 16:09:44 2010 +0200
1.3 @@ -221,12 +221,12 @@
1.4      from unimodular_reduce_norm[OF th0] o
1.5      have "\<exists>v. cmod (complex_of_real (cmod b) / b + v^n) < 1"
1.6        apply (cases "cmod (complex_of_real (cmod b) / b + 1) < 1", rule_tac x="1" in exI, simp)
1.7 -      apply (cases "cmod (complex_of_real (cmod b) / b - 1) < 1", rule_tac x="-1" in exI, simp add: diff_def)
1.8 +      apply (cases "cmod (complex_of_real (cmod b) / b - 1) < 1", rule_tac x="-1" in exI, simp add: diff_minus)
1.9        apply (cases "cmod (complex_of_real (cmod b) / b + ii) < 1")
1.10        apply (cases "even m", rule_tac x="ii" in exI, simp add: m power_mult)
1.11        apply (rule_tac x="- ii" in exI, simp add: m power_mult)
1.12 -      apply (cases "even m", rule_tac x="- ii" in exI, simp add: m power_mult diff_def)
1.13 -      apply (rule_tac x="ii" in exI, simp add: m power_mult diff_def)
1.14 +      apply (cases "even m", rule_tac x="- ii" in exI, simp add: m power_mult diff_minus)
1.15 +      apply (rule_tac x="ii" in exI, simp add: m power_mult diff_minus)
1.16        done
1.17      then obtain v where v: "cmod (complex_of_real (cmod b) / b + v^n) < 1" by blast
1.18      let ?w = "v / complex_of_real (root n (cmod b))"
1.19 @@ -959,7 +959,7 @@
1.20
1.21  lemma mpoly_sub_conv:
1.22    "poly p (x::complex) - poly q x \<equiv> poly p x + -1 * poly q x"
1.23 -  by (simp add: diff_def)
1.24 +  by (simp add: diff_minus)
1.25
1.26  lemma poly_pad_rule: "poly p x = 0 ==> poly (pCons 0 p) x = (0::complex)" by simp
1.27
```