author | wenzelm |
Fri, 01 Sep 1995 14:27:36 +0200 | |
changeset 1247 | 18b1441fb603 |
child 2907 | 0e272e4c7cb2 |
permissions | -rw-r--r-- |
1247 | 1 |
(* Title: Group.thy |
2 |
ID: $Id$ |
|
3 |
Author: Markus Wenzel, TU Muenchen |
|
4 |
*) |
|
5 |
||
6 |
Group = Sigs + Set + |
|
7 |
||
8 |
(* semigroups *) |
|
9 |
||
10 |
axclass |
|
11 |
semigroup < times |
|
12 |
assoc "(x * y) * z = x * (y * z)" |
|
13 |
||
14 |
||
15 |
(* groups *) |
|
16 |
||
17 |
axclass |
|
18 |
group < one, inv, semigroup |
|
19 |
left_unit "1 * x = x" |
|
20 |
left_inv "inv x * x = 1" |
|
21 |
||
22 |
||
23 |
(* abelian groups *) |
|
24 |
||
25 |
axclass |
|
26 |
agroup < group |
|
27 |
commut "x * y = y * x" |
|
28 |
||
29 |
end |