diff -r d00b01ed8539 -r af5e09b6c208 src/HOL/AxClasses/Tutorial/Semigroup.thy --- 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