diff -r 706cfddca75c -r 18b1441fb603 src/HOL/AxClasses/Tutorial/MonoidGroupInsts.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/AxClasses/Tutorial/MonoidGroupInsts.thy	Fri Sep 01 14:27:36 1995 +0200
@@ -0,0 +1,22 @@
+(*  Title:      HOL/AxClass/Tutorial/MonoidGroupInsts.thy
+    ID:         $Id$
+    Author:     Markus Wenzel, TU Muenchen
+
+Add derived class inclusions monoid < semigroup and group < monoid to
+type signature -- some kind of 'abstract instantiations'.
+*)
+
+MonoidGroupInsts = Monoid + Group +
+
+(* monoids are semigroups *)
+
+instance
+  monoid < semigroup            (Monoid.assoc)
+
+
+(* groups are monoids *)
+
+instance
+  group < monoid                (assoc, left_unit, right_unit)
+
+end