updated class documentation

--- a/doc-src/IsarAdvanced/Classes/Thy/Classes.thy	Sun Feb 01 19:59:20 2009 +0100
+++ b/doc-src/IsarAdvanced/Classes/Thy/Classes.thy	Mon Feb 02 09:01:14 2009 +0100
@@ -106,7 +106,7 @@
   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)"
 
@@ -349,7 +349,7 @@
   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"
 
@@ -541,7 +541,7 @@
      \label{fig:subclass}
    \end{center}
   \end{figure}
-
+7
   For illustration, a derived definition
   in @{text group} which uses @{text pow_nat}:
 *}
@@ -583,7 +583,9 @@
   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,
@@ -613,4 +615,21 @@
 
 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

--- a/doc-src/IsarAdvanced/Classes/Thy/document/Classes.tex	Sun Feb 01 19:59:20 2009 +0100
+++ b/doc-src/IsarAdvanced/Classes/Thy/document/Classes.tex	Mon Feb 02 09:01:14 2009 +0100
@@ -137,7 +137,7 @@
 %
 \isatagquote
 \isacommand{class}\isamarkupfalse%
-\ semigroup\ {\isacharequal}\ type\ {\isacharplus}\isanewline
+\ semigroup\ {\isacharequal}\isanewline
 \ \ \isakeyword{fixes}\ mult\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isasymalpha}\ {\isasymRightarrow}\ {\isasymalpha}\ {\isasymRightarrow}\ {\isasymalpha}{\isachardoublequoteclose}\ \ \ \ {\isacharparenleft}\isakeyword{infixl}\ {\isachardoublequoteopen}{\isasymotimes}{\isachardoublequoteclose}\ {\isadigit{7}}{\isadigit{0}}{\isacharparenright}\isanewline
 \ \ \isakeyword{assumes}\ assoc{\isacharcolon}\ {\isachardoublequoteopen}{\isacharparenleft}x\ {\isasymotimes}\ y{\isacharparenright}\ {\isasymotimes}\ z\ {\isacharequal}\ x\ {\isasymotimes}\ {\isacharparenleft}y\ {\isasymotimes}\ z{\isacharparenright}{\isachardoublequoteclose}%
 \endisatagquote
@@ -583,7 +583,7 @@
 %
 \isatagquote
 \isacommand{class}\isamarkupfalse%
-\ idem\ {\isacharequal}\ type\ {\isacharplus}\isanewline
+\ idem\ {\isacharequal}\isanewline
 \ \ \isakeyword{fixes}\ f\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isasymalpha}\ {\isasymRightarrow}\ {\isasymalpha}{\isachardoublequoteclose}\isanewline
 \ \ \isakeyword{assumes}\ idem{\isacharcolon}\ {\isachardoublequoteopen}f\ {\isacharparenleft}f\ x{\isacharparenright}\ {\isacharequal}\ f\ x{\isachardoublequoteclose}%
 \endisatagquote
@@ -1014,7 +1014,7 @@
      \label{fig:subclass}
    \end{center}
   \end{figure}
-
+7
   For illustration, a derived definition
   in \isa{group} which uses \isa{pow{\isacharunderscore}nat}:%
 \end{isamarkuptext}%
@@ -1099,7 +1099,11 @@
 \end{isamarkuptext}%
 \isamarkuptrue%
 %
-\isamarkupsection{Type classes and code generation%
+\isamarkupsection{Further issues%
+}
+\isamarkuptrue%
+%
+\isamarkupsubsection{Type classes and code generation%
 }
 \isamarkuptrue%
 %
@@ -1301,6 +1305,26 @@
 %
 \endisadelimquote
 %
+\isamarkupsubsection{Inspecting the type class universe%
+}
+\isamarkuptrue%
+%
+\begin{isamarkuptext}%
+To facilitate orientation in complex subclass structures,
+  two diagnostics commands are provided:
+
+  \begin{description}
+
+    \item[\hyperlink{command.print-classes}{\mbox{\isa{\isacommand{print{\isacharunderscore}classes}}}}] print a list of all classes
+      together with associated operations etc.
+
+    \item[\hyperlink{command.class-deps}{\mbox{\isa{\isacommand{class{\isacharunderscore}deps}}}}] visualizes the subclass relation
+      between all classes as a Hasse diagram.
+
+  \end{description}%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
 \isadelimtheory
 %
 \endisadelimtheory

--- a/src/HOL/ex/PresburgerEx.thy	Sun Feb 01 19:59:20 2009 +0100
+++ b/src/HOL/ex/PresburgerEx.thy	Mon Feb 02 09:01:14 2009 +0100
@@ -1,5 +1,4 @@
 (*  Title:      HOL/ex/PresburgerEx.thy
-    ID:         $Id$
     Author:     Amine Chaieb, TU Muenchen
 *)