src/HOL/Library/Polynomial.thy
changeset 57862 8f074e6e22fc
parent 57512 cc97b347b301
child 58199 5fbe474b5da8
     1.1 --- a/src/HOL/Library/Polynomial.thy	Tue Aug 05 12:42:38 2014 +0200
     1.2 +++ b/src/HOL/Library/Polynomial.thy	Tue Aug 05 12:56:15 2014 +0200
     1.3 @@ -1315,8 +1315,7 @@
     1.4      then have "finite {x. poly k x = 0}" using `k \<noteq> 0` by (rule Suc.hyps)
     1.5      then have "finite (insert a {x. poly k x = 0})" by simp
     1.6      then show "finite {x. poly p x = 0}"
     1.7 -      by (simp add: k uminus_add_conv_diff Collect_disj_eq
     1.8 -               del: mult_pCons_left)
     1.9 +      by (simp add: k Collect_disj_eq del: mult_pCons_left)
    1.10    qed
    1.11  qed
    1.12