src/HOL/Isar_Examples/Group.thy

  \idt{one} :: \alpha, \idt{inverse} :: \alpha \To \alpha)$ are defined
  as an axiomatic type class as follows.  Note that the parent class
  $\idt{times}$ is provided by the basic HOL theory.
 *}
 
-consts
-  one :: "'a"
-  inverse :: "'a => 'a"
-
-axclass
-  group < times
-  group_assoc:         "(x * y) * z = x * (y * z)"
-  group_left_one:      "one * x = x"
-  group_left_inverse:  "inverse x * x = one"
+notation Groups.one ("one")
+
+class group = times + one + inverse +
+  assumes group_assoc:         "(x * y) * z = x * (y * z)"
+  assumes group_left_one:      "one * x = x"
+  assumes group_left_inverse:  "inverse x * x = one"
 
 text {*
  The group axioms only state the properties of left one and inverse,
  the right versions may be derived as follows.
 *}

 text {*
  Monoids over signature $({\times} :: \alpha \To \alpha \To \alpha,
  \idt{one} :: \alpha)$ are defined like this.
 *}
 
-axclass monoid < times
-  monoid_assoc:       "(x * y) * z = x * (y * z)"
-  monoid_left_one:   "one * x = x"
-  monoid_right_one:  "x * one = x"
+class monoid = times + one +
+  assumes monoid_assoc:       "(x * y) * z = x * (y * z)"
+  assumes monoid_left_one:   "one * x = x"
+  assumes monoid_right_one:  "x * one = x"
 
 text {*
  Groups are \emph{not} yet monoids directly from the definition.  For
  monoids, \name{right-one} had to be included as an axiom, but for
  groups both \name{right-one} and \name{right-inverse} are derivable