Changes to HOL/Algebra:
- Axclasses consolidated (axiom one_not_zero).
- Now uses summation operator setsum; SUM has been removed.
- Priority of infix assoc changed to 50, in accordance to dvd.
(*
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