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

   Depending on an arbitrary type @{text "\<alpha>"}, class @{text
   "semigroup"} introduces a binary operator @{text "(\<otimes>)"} that is
   assumed to be associative:
 *}
 
-class %quote semigroup = type +
+class %quote semigroup =
   fixes mult :: "\<alpha> \<Rightarrow> \<alpha> \<Rightarrow> \<alpha>"    (infixl "\<otimes>" 70)
   assumes assoc: "(x \<otimes> y) \<otimes> z = x \<otimes> (y \<otimes> z)"
 
 text {*
   \noindent This @{command 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 %quote idem = type +
+class %quote idem =
   fixes f :: "\<alpha> \<Rightarrow> \<alpha>"
   assumes idem: "f (f x) = f x"
 
 text {*
   \noindent essentially introduces the locale

         before and after establishing the relationship
         @{text "group \<subseteq> monoid"};  transitive edges left out.}
      \label{fig:subclass}
    \end{center}
   \end{figure}
-
+7
   For illustration, a derived definition
   in @{text group} which uses @{text pow_nat}:
 *}
 
 definition %quote (in group) pow_int :: "int \<Rightarrow> \<alpha> \<Rightarrow> \<alpha>" where

   enforces the global class operation @{text "mult [nat]"}.
   In the global context in example 3, the reference is
   to the polymorphic global class operation @{text "mult [?\<alpha> \<Colon> semigroup]"}.
 *}
 
-section {* Type classes and code generation *}
+section {* Further issues *}
+
+subsection {* Type classes and code generation *}
 
 text {*
   Turning back to the first motivation for type classes,
   namely overloading, it is obvious that overloading
   stemming from @{command class} statements and

   \noindent The whole code in SML with explicit dictionary passing:
 *}
 
 text %quote {*@{code_stmts example (SML)}*}
 
+subsection {* Inspecting the type class universe *}
+
+text {*
+  To facilitate orientation in complex subclass structures,
+  two diagnostics commands are provided:
+
+  \begin{description}
+
+    \item[@{command "print_classes"}] print a list of all classes
+      together with associated operations etc.
+
+    \item[@{command "class_deps"}] visualizes the subclass relation
+      between all classes as a Hasse diagram.
+
+  \end{description}
+*}
+
 end