doc-src/IsarAdvanced/Classes/Thy/Classes.thy

   Depending on an arbitrary type @{text "\<alpha>"}, class @{text
   "semigroup"} introduces a binary operation @{text "\<circ>"} that is
   assumed to be associative:
 *}
 
-    class semigroup =
+    class semigroup = type +
       fixes mult :: "\<alpha> \<Rightarrow> \<alpha> \<Rightarrow> \<alpha>"    (infixl "\<^loc>\<otimes>" 70)
       assumes assoc: "(x \<^loc>\<otimes> y) \<^loc>\<otimes> z = x \<^loc>\<otimes> (y \<^loc>\<otimes> z)"
 
 text {*
   \noindent This @{text "\<CLASS>"} specification consists of two

   in practice.  As stated in the introduction, classes also provide
   a link to Isar's locale system.  Indeed, the logical core of a class
   is nothing else than a locale:
 *}
 
-class idem =
+class idem = type +
   fixes f :: "\<alpha> \<Rightarrow> \<alpha>"
   assumes idem: "f (f x) = f x"
 
 text {*
   \noindent essentially introduces the locale