(* Sums with naturals as index domain $Id$ Author: Clemens Ballarin, started 12 December 1996 *) NatSum = Ring + instance ring < plus_ac0 (a_assoc, a_comm, l_zero) end