--- a/src/HOL/Library/Fundamental_Theorem_Algebra.thy Mon Jul 19 16:09:44 2010 +0200
+++ b/src/HOL/Library/Fundamental_Theorem_Algebra.thy Mon Jul 19 16:09:44 2010 +0200
@@ -221,12 +221,12 @@
from unimodular_reduce_norm[OF th0] o
have "\<exists>v. cmod (complex_of_real (cmod b) / b + v^n) < 1"
apply (cases "cmod (complex_of_real (cmod b) / b + 1) < 1", rule_tac x="1" in exI, simp)
- apply (cases "cmod (complex_of_real (cmod b) / b - 1) < 1", rule_tac x="-1" in exI, simp add: diff_def)
+ apply (cases "cmod (complex_of_real (cmod b) / b - 1) < 1", rule_tac x="-1" in exI, simp add: diff_minus)
apply (cases "cmod (complex_of_real (cmod b) / b + ii) < 1")
apply (cases "even m", rule_tac x="ii" in exI, simp add: m power_mult)
apply (rule_tac x="- ii" in exI, simp add: m power_mult)
- apply (cases "even m", rule_tac x="- ii" in exI, simp add: m power_mult diff_def)
- apply (rule_tac x="ii" in exI, simp add: m power_mult diff_def)
+ apply (cases "even m", rule_tac x="- ii" in exI, simp add: m power_mult diff_minus)
+ apply (rule_tac x="ii" in exI, simp add: m power_mult diff_minus)
done
then obtain v where v: "cmod (complex_of_real (cmod b) / b + v^n) < 1" by blast
let ?w = "v / complex_of_real (root n (cmod b))"
@@ -959,7 +959,7 @@
lemma mpoly_sub_conv:
"poly p (x::complex) - poly q x \<equiv> poly p x + -1 * poly q x"
- by (simp add: diff_def)
+ by (simp add: diff_minus)
lemma poly_pad_rule: "poly p x = 0 ==> poly (pCons 0 p) x = (0::complex)" by simp