src/Doc/Isar_Ref/Spec.thy

     ;
     @@{command instance} (() | (@{syntax nameref} + @'and') '::' @{syntax arity} |
       @{syntax nameref} ('<' | '\<subseteq>') @{syntax nameref} )
     ;
     @@{command subclass} @{syntax target}? @{syntax nameref}
+    ;
+    @@{command class_deps} @{syntax sort}? @{syntax sort}?
   \<close>}
 
   \begin{description}
 
   \item @{command "class"}~@{text "c = superclasses + body"} defines

 
   \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.
+  subclass relations as a Hasse diagram.  An optional first sort argument
+  constrains the set of classes to all subclasses of this sort,
+  an optional second sort argument to all superclasses of this sort.
 
   \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,