author | wenzelm |
Tue, 12 Dec 2006 11:57:30 +0100 | |
changeset 21788 | d460465a9f97 |
parent 16417 | 9bc16273c2d4 |
permissions | -rw-r--r-- |
10134 | 1 |
(* Title: HOL/AxClasses/Semigroups.thy |
2 |
ID: $Id$ |
|
3 |
Author: Markus Wenzel, TU Muenchen |
|
4 |
*) |
|
5 |
||
16417 | 6 |
theory Semigroups imports Main begin |
10134 | 7 |
|
8 |
consts |
|
9 |
times :: "'a => 'a => 'a" (infixl "[*]" 70) |
|
10 |
||
12338
de0f4a63baa5
renamed class "term" to "type" (actually "HOL.type");
wenzelm
parents:
10681
diff
changeset
|
11 |
axclass semigroup < type |
10134 | 12 |
assoc: "(x [*] y) [*] z = x [*] (y [*] z)" |
13 |
||
14 |
||
15 |
consts |
|
16 |
plus :: "'a => 'a => 'a" (infixl "[+]" 70) |
|
17 |
||
12338
de0f4a63baa5
renamed class "term" to "type" (actually "HOL.type");
wenzelm
parents:
10681
diff
changeset
|
18 |
axclass plus_semigroup < type |
10134 | 19 |
assoc: "(x [+] y) [+] z = x [+] (y [+] z)" |
20 |
||
21 |
end |