changeset 12338 | de0f4a63baa5 |
parent 10681 | ec76e17f73c5 |
child 14981 | e73f8140af78 |
--- a/src/HOL/AxClasses/Semigroups.thy Sat Dec 01 18:51:46 2001 +0100 +++ b/src/HOL/AxClasses/Semigroups.thy Sat Dec 01 18:52:32 2001 +0100 @@ -9,14 +9,14 @@ consts times :: "'a => 'a => 'a" (infixl "[*]" 70) -axclass semigroup < "term" +axclass semigroup < type assoc: "(x [*] y) [*] z = x [*] (y [*] z)" consts plus :: "'a => 'a => 'a" (infixl "[+]" 70) -axclass plus_semigroup < "term" +axclass plus_semigroup < type assoc: "(x [+] y) [+] z = x [+] (y [+] z)" end