src/HOL/Algebra/FiniteProduct.thy
changeset 28524 644b62cf678f
parent 27933 4b867f6a65d3
child 29237 e90d9d51106b
     1.1 --- a/src/HOL/Algebra/FiniteProduct.thy	Tue Oct 07 16:07:40 2008 +0200
     1.2 +++ b/src/HOL/Algebra/FiniteProduct.thy	Tue Oct 07 16:07:50 2008 +0200
     1.3 @@ -291,7 +291,7 @@
     1.4    finprod :: "[('b, 'm) monoid_scheme, 'a => 'b, 'a set] => 'b"
     1.5    "finprod G f A == if finite A
     1.6        then foldD (carrier G) (mult G o f) \<one> A
     1.7 -      else arbitrary"
     1.8 +      else undefined"
     1.9  
    1.10  syntax
    1.11    "_finprod" :: "index => idt => 'a set => 'b => 'b"