doc-src/IsarRef/Thy/Spec.thy

     @{command_def "class"} & : & @{text "theory \<rightarrow> local_theory"} \\
     @{command_def "instantiation"} & : & @{text "theory \<rightarrow> local_theory"} \\
     @{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}
 
   \begin{rail}
     'class' name '=' ((superclassexpr '+' (contextelem+)) | superclassexpr | (contextelem+)) \\

     'instance'
     ;
     'subclass' target? nameref
     ;
     'print\_classes'
+    ;
+    'class\_deps'
     ;
 
     superclassexpr: nameref | (nameref '+' superclassexpr)
     ;
   \end{rail}

   @{text d} is proven to be subclass @{text c} and the locale @{text
   c} is interpreted into @{text d} simultaneously.
 
   \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
   default proof step (e.g.\ of @{command "proof"}).  In particular,