# HG changeset patch
# User nipkow
# Date 1182777574 -7200
# Node ID 94e7c8f823b55be0da46d94377eb9e1381afde5f
# Parent  84e9216a6d0efa24ab4a932d8b1d287fda6bcf91
removed redundant lemma

diff -r 84e9216a6d0e -r 94e7c8f823b5 src/HOL/Hyperreal/Poly.thy
--- a/src/HOL/Hyperreal/Poly.thy	Mon Jun 25 15:19:18 2007 +0200
+++ b/src/HOL/Hyperreal/Poly.thy	Mon Jun 25 15:19:34 2007 +0200
@@ -870,7 +870,7 @@
 apply (rule_tac x = "inverse (real (Suc n)) %* (qa +++ -- (pderiv q))" in exI)
 apply (subgoal_tac "poly ([-a, 1] %^ n *** q) = poly ([-a, 1] %^ n *** ([-a, 1] *** (inverse (real (Suc n)) %* (qa +++ -- (pderiv q))))) ")
 apply (drule poly_mult_left_cancel [THEN iffD1], simp)
-apply (simp add: fun_eq poly_mult poly_add poly_cmult poly_minus del: pmult_Cons mult_cancel_left field_mult_cancel_left, safe)
+apply (simp add: fun_eq poly_mult poly_add poly_cmult poly_minus del: pmult_Cons mult_cancel_left, safe)
 apply (rule_tac c1 = "real (Suc n)" in real_mult_left_cancel [THEN iffD1])
 apply (simp (no_asm))
 apply (subgoal_tac "real (Suc n) * (poly ([- a, 1] %^ n) xa * poly q xa) =