Strange enough, the current definitions of OrderedAbelianSemiGroup and OrderedAbelianMonoid coincide:

  )abbrev category OASGP OrderedAbelianSemiGroup
  ++ Ordered sets which are also abelian semigroups, such that the addition
  ++ preserves the ordering.
  ++   \spad{ x < y => x+z < y+z}

  OrderedAbelianSemiGroup(): Category == Join(OrderedSet, AbelianMonoid)

  )abbrev category OAMON OrderedAbelianMonoid
  ++ Ordered sets which are also abelian monoids, such that the addition
  ++ preserves the ordering.

  OrderedAbelianMonoid(): Category ==
          Join(OrderedAbelianSemiGroup, AbelianMonoid)

The definition of OASGP should read:

    OrderedAbelianSemiGroup(): Category == Join(OrderedSet, AbelianSemiGroup)

Martin

This is a very deep change and I'm going to have to devote a fair bit of time to testing the system before this one gets released into the wild.

Tim

Furthermore, we should have:

    PositiveInteger: Join(OrderedAbelianSemiGroup,Monoid) with

instead of:

    PositiveInteger: Join(AbelianSemiGroup,OrderedSet,Monoid)

as Waldek noticed...

Martin

Fixed in OpenAxiom