Put in minimal simpset to avoid excessive simplification,
just as in revision 1.9 of HOL/indrule.ML
(* Title: HOL/AxClasses/Tutorial/Semigroup.thy
ID: $Id$
Author: Markus Wenzel, TU Muenchen
Define class "semigroup".
*)
Semigroup = HOL +
consts
"<*>" :: "['a, 'a] => 'a" (infixl 70)
axclass
semigroup < term
assoc "(x <*> y) <*> z = x <*> (y <*> z)"
end