src/HOL/AxClasses/Tutorial/Monoid.thy

new theorem leadsTo_refl and induction rule leadsTo_induct_pre

(*  Title:      HOL/AxClasses/Tutorial/Monoid.thy
    ID:         $Id$
    Author:     Markus Wenzel, TU Muenchen

Define class "monoid".
*)

Monoid = Sigs +

(* monoids *)

axclass
  monoid < term
  assoc         "(x <*> y) <*> z = x <*> (y <*> z)"
  left_unit     "1 <*> x = x"
  right_unit    "x <*> 1 = x"

end