changeset 10135 | c2a4dccf6e67 |
parent 10134 | 537206cc738f |
child 10136 | ed576de7bddc |
10134:537206cc738f | 10135:c2a4dccf6e67 |
---|---|
1 (* Title: Group.thy |
|
2 ID: $Id$ |
|
3 Author: Markus Wenzel, TU Muenchen |
|
4 *) |
|
5 |
|
6 Group = Sigs + Fun + |
|
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, inverse, semigroup |
|
19 left_unit "1 * x = x" |
|
20 left_inverse "inverse x * x = 1" |
|
21 |
|
22 |
|
23 (* abelian groups *) |
|
24 |
|
25 axclass |
|
26 agroup < group |
|
27 commut "x * y = y * x" |
|
28 |
|
29 end |