# HG changeset patch
# User haftmann
# Date 1233563274 -3600
# Node ID 10e6f2faa1e5df0b9678794743546c4805f691f3
# Parent  a1ecdd8cf81c42628285e70fcd5b1537838fa551
updated type class section

diff -r a1ecdd8cf81c -r 10e6f2faa1e5 doc-src/IsarRef/Thy/Spec.thy
--- a/doc-src/IsarRef/Thy/Spec.thy	Mon Feb 02 09:01:14 2009 +0100
+++ b/doc-src/IsarRef/Thy/Spec.thy	Mon Feb 02 09:27:54 2009 +0100
@@ -569,6 +569,7 @@
     @{command_def "instance"} & : & @{text "local_theory \<rightarrow> local_theory"} \\
     @{command_def "subclass"} & : & @{text "local_theory \<rightarrow> local_theory"} \\
     @{command_def "print_classes"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\
+    @{command_def "class_deps"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\
     @{method_def intro_classes} & : & @{text method} \\
   \end{matharray}
 
@@ -584,6 +585,8 @@
     ;
     'print\_classes'
     ;
+    'class\_deps'
+    ;
 
     superclassexpr: nameref | (nameref '+' superclassexpr)
     ;
@@ -637,6 +640,9 @@
   \item @{command "print_classes"} prints all classes in the current
   theory.
 
+  \item @{command "class_deps"} visualizes all classes and their
+  subclass relations as a Hasse diagram.
+
   \item @{method intro_classes} repeatedly expands all class
   introduction rules of this theory.  Note that this method usually
   needs not be named explicitly, as it is already included in the
diff -r a1ecdd8cf81c -r 10e6f2faa1e5 doc-src/IsarRef/Thy/document/Spec.tex
--- a/doc-src/IsarRef/Thy/document/Spec.tex	Mon Feb 02 09:01:14 2009 +0100
+++ b/doc-src/IsarRef/Thy/document/Spec.tex	Mon Feb 02 09:27:54 2009 +0100
@@ -583,6 +583,7 @@
     \indexdef{}{command}{instance}\hypertarget{command.instance}{\hyperlink{command.instance}{\mbox{\isa{\isacommand{instance}}}}} & : & \isa{{\isachardoublequote}local{\isacharunderscore}theory\ {\isasymrightarrow}\ local{\isacharunderscore}theory{\isachardoublequote}} \\
     \indexdef{}{command}{subclass}\hypertarget{command.subclass}{\hyperlink{command.subclass}{\mbox{\isa{\isacommand{subclass}}}}} & : & \isa{{\isachardoublequote}local{\isacharunderscore}theory\ {\isasymrightarrow}\ local{\isacharunderscore}theory{\isachardoublequote}} \\
     \indexdef{}{command}{print\_classes}\hypertarget{command.print-classes}{\hyperlink{command.print-classes}{\mbox{\isa{\isacommand{print{\isacharunderscore}classes}}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isa{{\isachardoublequote}context\ {\isasymrightarrow}{\isachardoublequote}} \\
+    \indexdef{}{command}{class\_deps}\hypertarget{command.class-deps}{\hyperlink{command.class-deps}{\mbox{\isa{\isacommand{class{\isacharunderscore}deps}}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isa{{\isachardoublequote}context\ {\isasymrightarrow}{\isachardoublequote}} \\
     \indexdef{}{method}{intro\_classes}\hypertarget{method.intro-classes}{\hyperlink{method.intro-classes}{\mbox{\isa{intro{\isacharunderscore}classes}}}} & : & \isa{method} \\
   \end{matharray}
 
@@ -598,6 +599,8 @@
     ;
     'print\_classes'
     ;
+    'class\_deps'
+    ;
 
     superclassexpr: nameref | (nameref '+' superclassexpr)
     ;
@@ -643,6 +646,9 @@
   \item \hyperlink{command.print-classes}{\mbox{\isa{\isacommand{print{\isacharunderscore}classes}}}} prints all classes in the current
   theory.
 
+  \item \hyperlink{command.class-deps}{\mbox{\isa{\isacommand{class{\isacharunderscore}deps}}}} visualizes all classes and their
+  subclass relations as a Hasse diagram.
+
   \item \hyperlink{method.intro-classes}{\mbox{\isa{intro{\isacharunderscore}classes}}} repeatedly expands all class
   introduction rules of this theory.  Note that this method usually
   needs not be named explicitly, as it is already included in the