equal
deleted
inserted
replaced
211 ("(3\<Oplus>__\<in>_. _)" [1000, 0, 51, 10] 10) |
211 ("(3\<Oplus>__\<in>_. _)" [1000, 0, 51, 10] 10) |
212 syntax (HTML output) |
212 syntax (HTML output) |
213 "_finsum" :: "index => idt => 'a set => 'b => 'b" |
213 "_finsum" :: "index => idt => 'a set => 'b => 'b" |
214 ("(3\<Oplus>__\<in>_. _)" [1000, 0, 51, 10] 10) |
214 ("(3\<Oplus>__\<in>_. _)" [1000, 0, 51, 10] 10) |
215 translations |
215 translations |
216 "\<Oplus>\<index>i:A. b" == "finsum \<struct>\<index> (%i. b) A" |
216 "\<Oplus>\<index>i:A. b" == "CONST finsum \<struct>\<index> (%i. b) A" |
217 -- {* Beware of argument permutation! *} |
217 -- {* Beware of argument permutation! *} |
218 |
218 |
219 context abelian_monoid begin |
219 context abelian_monoid begin |
220 |
220 |
221 (* |
221 (* |