diff -r 706cfddca75c -r 18b1441fb603 src/HOL/AxClasses/Tutorial/Monoid.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/AxClasses/Tutorial/Monoid.thy	Fri Sep 01 14:27:36 1995 +0200
@@ -0,0 +1,18 @@
+(*  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