--- 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
--- 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