Put in minimal simpset to avoid excessive simplification,
just as in revision 1.9 of HOL/indrule.ML
(* Title: Monoid.thy
ID: $Id$
Author: Markus Wenzel, TU Muenchen
*)
Monoid = Sigs +
(* monoids *)
axclass
monoid < times, one
assoc "(x * y) * z = x * (y * z)"
left_unit "1 * x = x"
right_unit "x * 1 = x"
end