src/HOL/Algebra/FiniteProduct.thy
 changeset 15095 63f5f4c265dd parent 14750 8f1ee65bd3ea child 15328 35951e6a7855
```     1.1 --- a/src/HOL/Algebra/FiniteProduct.thy	Sat Jul 31 20:54:23 2004 +0200
1.2 +++ b/src/HOL/Algebra/FiniteProduct.thy	Mon Aug 02 09:44:46 2004 +0200
1.3 @@ -283,7 +283,7 @@
1.4  subsection {* Products over Finite Sets *}
1.5
1.6  constdefs (structure G)
1.7 -  finprod :: "[_, 'a => 'b, 'a set] => 'b"
1.8 +  finprod :: "[('b, 'm) monoid_scheme, 'a => 'b, 'a set] => 'b"
1.9    "finprod G f A == if finite A
1.10        then foldD (carrier G) (mult G o f) \<one> A
1.11        else arbitrary"
1.12 @@ -298,7 +298,8 @@
1.13    "_finprod" :: "index => idt => 'a set => 'b => 'b"
1.14        ("(3\<Otimes>__\<in>_. _)" [1000, 0, 51, 10] 10)
1.15  translations
1.16 -  "\<Otimes>\<index>i:A. b" == "finprod \<struct>\<index> (%i. b) A"  -- {* Beware of argument permutation! *}
1.17 +  "\<Otimes>\<index>i:A. b" == "finprod \<struct>\<index> (%i. b) A"
1.18 +  -- {* Beware of argument permutation! *}
1.19
1.20  ML_setup {*
1.21    simpset_ref() := simpset() setsubgoaler asm_full_simp_tac;
1.22 @@ -402,9 +403,8 @@
1.23    from insert have ga: "g a \<in> carrier G" by fast
1.24    from insert have fgA: "(%x. f x \<otimes> g x) \<in> A -> carrier G"