src/HOL/Finite_Set.thy

 constdefs
   setsum :: "('a => 'b) => 'a set => 'b::comm_monoid_add"
   "setsum f A == if finite A then fold (op +) f 0 A else 0"
 
 abbreviation
-  Setsum  ("\<Sum>_" [1000] 999)
+  Setsum  ("\<Sum>_" [1000] 999) where
   "\<Sum>A == setsum (%x. x) A"
 
 text{* Now: lot's of fancy syntax. First, @{term "setsum (%x. e) A"} is
 written @{text"\<Sum>x\<in>A. e"}. *}
 

 constdefs
   setprod :: "('a => 'b) => 'a set => 'b::comm_monoid_mult"
   "setprod f A == if finite A then fold (op *) f 1 A else 1"
 
 abbreviation
-  Setprod  ("\<Prod>_" [1000] 999)
+  Setprod  ("\<Prod>_" [1000] 999) where
   "\<Prod>A == setprod (%x. x) A"
 
 syntax
   "_setprod" :: "pttrn => 'a set => 'b => 'b::comm_monoid_mult"  ("(3PROD _:_. _)" [0, 51, 10] 10)
 syntax (xsymbols)