src/Doc/Isar_Ref/Spec.thy
changeset 59422 db6ecef63d5b
parent 59320 a375de4dc07a
child 59781 a71dbf3481a2
--- a/src/Doc/Isar_Ref/Spec.thy	Wed Jan 21 18:40:02 2015 +0100
+++ b/src/Doc/Isar_Ref/Spec.thy	Wed Jan 21 18:40:03 2015 +0100
@@ -915,7 +915,8 @@
     ;
     @@{command subclass} @{syntax target}? @{syntax nameref}
     ;
-    @@{command class_deps} @{syntax sort}? @{syntax sort}?
+    @@{command class_deps} ( ( @{syntax sort} | ( '(' ( @{syntax sort} + @'|' ) ')' ) ) \<newline>
+      ( @{syntax sort} | ( '(' ( @{syntax sort} + @'|' ) ')' ) )? )?
   \<close>}
 
   \begin{description}
@@ -979,9 +980,10 @@
   theory.
 
   \item @{command "class_deps"} visualizes all classes and their
-  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.
+  subclass relations as a Hasse diagram.  An optional first argument
+  constrains the set of classes to all subclasses of at least one given
+  sort, an optional second rgument to all superclasses of at least one given
+  sort.
 
   \item @{method intro_classes} repeatedly expands all class
   introduction rules of this theory.  Note that this method usually