equal
deleted
inserted
replaced
12 times :: "'a => 'a => 'a" (infixl "[*]" 70) |
12 times :: "'a => 'a => 'a" (infixl "[*]" 70) |
13 invers :: "'a => 'a" |
13 invers :: "'a => 'a" |
14 one :: 'a |
14 one :: 'a |
15 |
15 |
16 |
16 |
17 axclass monoid < "term" |
17 axclass monoid < type |
18 assoc: "(x [*] y) [*] z = x [*] (y [*] z)" |
18 assoc: "(x [*] y) [*] z = x [*] (y [*] z)" |
19 left_unit: "one [*] x = x" |
19 left_unit: "one [*] x = x" |
20 right_unit: "x [*] one = x" |
20 right_unit: "x [*] one = x" |
21 |
21 |
22 axclass semigroup < "term" |
22 axclass semigroup < type |
23 assoc: "(x [*] y) [*] z = x [*] (y [*] z)" |
23 assoc: "(x [*] y) [*] z = x [*] (y [*] z)" |
24 |
24 |
25 axclass group < semigroup |
25 axclass group < semigroup |
26 left_unit: "one [*] x = x" |
26 left_unit: "one [*] x = x" |
27 left_inverse: "invers x [*] x = one" |
27 left_inverse: "invers x [*] x = one" |