author | paulson |
Wed, 01 Feb 2006 15:22:02 +0100 | |
changeset 18886 | 9f27383426db |
parent 16417 | 9bc16273c2d4 |
permissions | -rw-r--r-- |
(* Title: HOL/AxClasses/Semigroups.thy ID: $Id$ Author: Markus Wenzel, TU Muenchen *) theory Semigroups imports Main begin consts times :: "'a => 'a => 'a" (infixl "[*]" 70) axclass semigroup < type assoc: "(x [*] y) [*] z = x [*] (y [*] z)" consts plus :: "'a => 'a => 'a" (infixl "[+]" 70) axclass plus_semigroup < type assoc: "(x [+] y) [+] z = x [+] (y [+] z)" end