| author | wenzelm |
| Sun, 16 Jul 2000 20:54:38 +0200 | |
| changeset 9363 | 86b48eafc70d |
| parent 8920 | af5e09b6c208 |
| child 10007 | 64bf7da1994a |
| permissions | -rw-r--r-- |
| 1247 | 1 |
(* Title: HOL/AxClasses/Tutorial/Semigroups.thy |
2 |
ID: $Id$ |
|
3 |
Author: Markus Wenzel, TU Muenchen |
|
4 |
*) |
|
5 |
||
| 8920 | 6 |
theory Semigroups = Main:; |
| 1247 | 7 |
|
8 |
consts |
|
| 8920 | 9 |
times :: "'a => 'a => 'a" (infixl "[*]" 70); |
| 1247 | 10 |
axclass |
| 8920 | 11 |
semigroup < "term" |
12 |
assoc: "(x [*] y) [*] z = x [*] (y [*] z)"; |
|
| 1247 | 13 |
|
| 8920 | 14 |
consts |
15 |
plus :: "'a => 'a => 'a" (infixl "[+]" 70); |
|
| 1247 | 16 |
axclass |
| 8920 | 17 |
plus_semigroup < "term" |
18 |
assoc: "(x [+] y) [+] z = x [+] (y [+] z)"; |
|
| 1247 | 19 |
|
| 8920 | 20 |
end; |