equal
deleted
inserted
replaced
306 else \<one>\<^bsub>G\<^esub>)" |
306 else \<one>\<^bsub>G\<^esub>)" |
307 |
307 |
308 syntax |
308 syntax |
309 "_finprod" :: "index \<Rightarrow> idt \<Rightarrow> 'a set \<Rightarrow> 'b \<Rightarrow> 'b" |
309 "_finprod" :: "index \<Rightarrow> idt \<Rightarrow> 'a set \<Rightarrow> 'b \<Rightarrow> 'b" |
310 ("(3\<Otimes>__\<in>_. _)" [1000, 0, 51, 10] 10) |
310 ("(3\<Otimes>__\<in>_. _)" [1000, 0, 51, 10] 10) |
|
311 syntax_consts |
|
312 "_finprod" \<rightleftharpoons> finprod |
311 translations |
313 translations |
312 "\<Otimes>\<^bsub>G\<^esub>i\<in>A. b" \<rightleftharpoons> "CONST finprod G (%i. b) A" |
314 "\<Otimes>\<^bsub>G\<^esub>i\<in>A. b" \<rightleftharpoons> "CONST finprod G (%i. b) A" |
313 \<comment> \<open>Beware of argument permutation!\<close> |
315 \<comment> \<open>Beware of argument permutation!\<close> |
314 |
316 |
315 lemma (in comm_monoid) finprod_empty [simp]: |
317 lemma (in comm_monoid) finprod_empty [simp]: |