src/HOL/AxClasses/Group/MonoidGroupInsts.thy
author clasohm
Tue, 21 Nov 1995 13:46:47 +0100
changeset 1357 dac9989eb88f
parent 1247 18b1441fb603
child 7651 e853cd3f3ede
permissions -rw-r--r--
replaced exit_use by exit_use_dir

(*  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