changeset 12338 | de0f4a63baa5 |
parent 11072 | 8f47967ecc80 |
child 14981 | e73f8140af78 |
--- a/src/HOL/AxClasses/Group.thy Sat Dec 01 18:51:46 2001 +0100 +++ b/src/HOL/AxClasses/Group.thy Sat Dec 01 18:52:32 2001 +0100 @@ -14,12 +14,12 @@ one :: 'a -axclass monoid < "term" +axclass monoid < type assoc: "(x [*] y) [*] z = x [*] (y [*] z)" left_unit: "one [*] x = x" right_unit: "x [*] one = x" -axclass semigroup < "term" +axclass semigroup < type assoc: "(x [*] y) [*] z = x [*] (y [*] z)" axclass group < semigroup