summary |
shortlog |
changelog |
graph |
tags |
branches |
files |
changeset |
file |
revisions |
annotate |
diff |
raw

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