author | wenzelm |
Fri, 15 Dec 2000 17:59:45 +0100 | |
changeset 10681 | ec76e17f73c5 |
parent 10134 | 537206cc738f |
child 12338 | de0f4a63baa5 |
permissions | -rw-r--r-- |
(* Title: HOL/AxClasses/Semigroups.thy ID: $Id$ Author: Markus Wenzel, TU Muenchen License: GPL (GNU GENERAL PUBLIC LICENSE) *) theory Semigroups = Main: consts times :: "'a => 'a => 'a" (infixl "[*]" 70) axclass semigroup < "term" assoc: "(x [*] y) [*] z = x [*] (y [*] z)" consts plus :: "'a => 'a => 'a" (infixl "[+]" 70) axclass plus_semigroup < "term" assoc: "(x [+] y) [+] z = x [+] (y [+] z)" end