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