equal
deleted
inserted
replaced
291 by (simp add: expand_poly_eq) |
291 by (simp add: expand_poly_eq) |
292 qed |
292 qed |
293 |
293 |
294 end |
294 end |
295 |
295 |
296 instance poly :: |
296 instance poly :: (cancel_comm_monoid_add) cancel_comm_monoid_add |
297 ("{cancel_ab_semigroup_add,comm_monoid_add}") cancel_ab_semigroup_add |
|
298 proof |
297 proof |
299 fix p q r :: "'a poly" |
298 fix p q r :: "'a poly" |
300 assume "p + q = p + r" thus "q = r" |
299 assume "p + q = p + r" thus "q = r" |
301 by (simp add: expand_poly_eq) |
300 by (simp add: expand_poly_eq) |
302 qed |
301 qed |