equal
deleted
inserted
replaced
216 show "- a + a = 0" by (simp add: fps_ext) |
216 show "- a + a = 0" by (simp add: fps_ext) |
217 show "a - b = a + - b" by (simp add: fps_ext) |
217 show "a - b = a + - b" by (simp add: fps_ext) |
218 qed |
218 qed |
219 |
219 |
220 instance fps :: (zero_neq_one) zero_neq_one |
220 instance fps :: (zero_neq_one) zero_neq_one |
221 by default (simp add: expand_fps_eq) |
221 by standard (simp add: expand_fps_eq) |
222 |
222 |
223 instance fps :: (semiring_0) semiring |
223 instance fps :: (semiring_0) semiring |
224 proof |
224 proof |
225 fix a b c :: "'a fps" |
225 fix a b c :: "'a fps" |
226 show "(a + b) * c = a * c + b * c" |
226 show "(a + b) * c = a * c + b * c" |