1.1 --- a/src/HOL/AxClasses/Group.thy Sat Dec 01 18:51:46 2001 +0100
1.2 +++ b/src/HOL/AxClasses/Group.thy Sat Dec 01 18:52:32 2001 +0100
1.3 @@ -14,12 +14,12 @@
1.4 one :: 'a
1.5
1.6
1.7 -axclass monoid < "term"
1.8 +axclass monoid < type
1.9 assoc: "(x [*] y) [*] z = x [*] (y [*] z)"
1.10 left_unit: "one [*] x = x"
1.11 right_unit: "x [*] one = x"
1.12
1.13 -axclass semigroup < "term"
1.14 +axclass semigroup < type
1.15 assoc: "(x [*] y) [*] z = x [*] (y [*] z)"
1.16
1.17 axclass group < semigroup