src/HOL/AxClasses/Tutorial/Monoid.thy

+(*  Title:      HOL/AxClasses/Tutorial/Monoid.thy
+    ID:         $Id$
+    Author:     Markus Wenzel, TU Muenchen
+
+Define class "monoid".
+*)
+
+Monoid = Sigs +
+
+(* monoids *)
+
+axclass
+  monoid < term
+  assoc         "(x <*> y) <*> z = x <*> (y <*> z)"
+  left_unit     "1 <*> x = x"
+  right_unit    "x <*> 1 = x"
+
+end