src/HOL/AxClasses/Group/MonoidGroupInsts.thy

Now Datatype.occs_in_prems prints the necessary warning ITSELF.

It is also easier to invoke and even works if the induction variable
is a parameter (rather than a free variable).

(*  Title:      MonoidGroupInsts.thy
    ID:         $Id$
    Author:     Markus Wenzel, TU Muenchen

Some class inclusions or 'abstract instantiations'.
*)

MonoidGroupInsts = Group + Monoid +


(* monoids are semigroups *)

instance
  monoid < semigroup            (Monoid.assoc)


(* groups are monoids *)

instance
  group < monoid                (assoc, left_unit, right_unit)

end