src/HOL/Algebra/FiniteProduct.thy
changeset 35847 19f1f7066917
parent 35416 d8d7d1b785af
child 35848 5443079512ea
     1.1 --- a/src/HOL/Algebra/FiniteProduct.thy	Sun Mar 21 06:59:23 2010 +0100
     1.2 +++ b/src/HOL/Algebra/FiniteProduct.thy	Sun Mar 21 15:57:40 2010 +0100
     1.3 @@ -285,11 +285,12 @@
     1.4  
     1.5  subsubsection {* Products over Finite Sets *}
     1.6  
     1.7 -constdefs (structure G)
     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 undefined"
    1.12 +definition
    1.13 +  finprod :: "[('b, 'm) monoid_scheme, 'a => 'b, 'a set] => 'b" where
    1.14 +  "finprod G f A ==
    1.15 +    if finite A
    1.16 +    then foldD (carrier G) (mult G o f) \<one>\<^bsub>G\<^esub> A
    1.17 +    else undefined"
    1.18  
    1.19  syntax
    1.20    "_finprod" :: "index => idt => 'a set => 'b => 'b"