--- a/src/HOL/Library/Fundamental_Theorem_Algebra.thy Thu Oct 31 16:54:22 2013 +0100
+++ b/src/HOL/Library/Fundamental_Theorem_Algebra.thy Fri Nov 01 18:51:14 2013 +0100
@@ -224,12 +224,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_minus)
+ apply (cases "cmod (complex_of_real (cmod b) / b - 1) < 1", rule_tac x="-1" in exI, simp del: minus_one add: minus_one [symmetric])
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_minus)
- apply (rule_tac x="ii" in exI, simp add: m power_mult diff_minus)
+ 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)
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))"
@@ -954,7 +954,7 @@
lemma mpoly_sub_conv:
"poly p (x::complex) - poly q x \<equiv> poly p x + -1 * poly q x"
- by (simp add: diff_minus)
+ by simp
lemma poly_pad_rule: "poly p x = 0 ==> poly (pCons 0 p) x = (0::complex)" by simp