| changeset 8920 | af5e09b6c208 |
| parent 8919 | d00b01ed8539 |
| child 8921 | 7c04c98132c4 |
| 8919:d00b01ed8539 | 8920:af5e09b6c208 |
|---|---|
1 (* Title: HOL/AxClasses/Tutorial/Semigroup.thy |
|
2 ID: $Id$ |
|
3 Author: Markus Wenzel, TU Muenchen |
|
4 |
|
5 Define class "semigroup". |
|
6 *) |
|
7 |
|
8 Semigroup = HOL + |
|
9 |
|
10 consts |
|
11 "<*>" :: "['a, 'a] => 'a" (infixl 70) |
|
12 |
|
13 axclass |
|
14 semigroup < term |
|
15 assoc "(x <*> y) <*> z = x <*> (y <*> z)" |
|
16 |
|
17 end |