src/HOL/Algebra/abstract/NatSum.thy
changeset 13735 7de9342aca7a
parent 13734 50dcee1c509e
child 13736 6ea0e7c43c4f
equal deleted inserted replaced
13734:50dcee1c509e 13735:7de9342aca7a
     1 (*
       
     2     Sums with naturals as index domain
       
     3     $Id$
       
     4     Author: Clemens Ballarin, started 12 December 1996
       
     5 *)
       
     6 
       
     7 NatSum = Ring +
       
     8 
       
     9 instance
       
    10   ring < plus_ac0 (a_assoc, a_comm, l_zero)
       
    11 
       
    12 end