src/HOL/AxClasses/Group/Monoid.thy

New record type of programs

(*  Title:      Monoid.thy
    ID:         $Id$
    Author:     Markus Wenzel, TU Muenchen
*)

Monoid = Sigs +

(* monoids *)

axclass
  monoid < times, one
  assoc         "(x * y) * z = x * (y * z)"
  left_unit     "1 * x = x"
  right_unit    "x * 1 = x"

end