src/HOL/Algebra/Ring.thy
changeset 35416 d8d7d1b785af
parent 35054 a5db9779b026
child 35847 19f1f7066917
     1.1 --- a/src/HOL/Algebra/Ring.thy	Wed Feb 24 11:55:52 2010 +0100
     1.2 +++ b/src/HOL/Algebra/Ring.thy	Mon Mar 01 13:40:23 2010 +0100
     1.3 @@ -198,8 +198,7 @@
     1.4    This definition makes it easy to lift lemmas from @{term finprod}.
     1.5  *}
     1.6  
     1.7 -constdefs
     1.8 -  finsum :: "[('b, 'm) ring_scheme, 'a => 'b, 'a set] => 'b"
     1.9 +definition finsum :: "[('b, 'm) ring_scheme, 'a => 'b, 'a set] => 'b" where
    1.10    "finsum G f A == finprod (| carrier = carrier G,
    1.11       mult = add G, one = zero G |) f A"
    1.12