src/HOL/AxClasses/Tutorial/Semigroup.thy
changeset 8920 af5e09b6c208
parent 8919 d00b01ed8539
child 8921 7c04c98132c4
--- a/src/HOL/AxClasses/Tutorial/Semigroup.thy	Mon May 22 13:20:47 2000 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,17 +0,0 @@
-(*  Title:      HOL/AxClasses/Tutorial/Semigroup.thy
-    ID:         $Id$
-    Author:     Markus Wenzel, TU Muenchen
-
-Define class "semigroup".
-*)
-
-Semigroup = HOL +
-
-consts
-  "<*>"         :: "['a, 'a] => 'a"             (infixl 70)
-
-axclass
-  semigroup < term
-  assoc         "(x <*> y) <*> z = x <*> (y <*> z)"
-
-end