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