src/Doc/IsarRef/Outer_Syntax.thy

     (in conjunction with @{verbatim "-l ZF"}, to specify the default
     logic image).  Note that option @{verbatim "-L"} does both
     of this at the same time.
   \end{warn}
 *}
+
+
+section {* Commands *}
+
+text {*
+  \begin{matharray}{rcl}
+    @{command_def "print_commands"}@{text "\<^sup>*"} & : & @{text "any \<rightarrow>"} \\
+    @{command_def "help"}@{text "\<^sup>*"} & : & @{text "any \<rightarrow>"} \\
+  \end{matharray}
+
+  @{rail "
+    @@{command help} (@{syntax name} * )
+  "}
+
+  \begin{description}
+
+  \item @{command "print_commands"} prints all outer syntax keywords
+  and commands.
+
+  \item @{command "help"}~@{text "pats"} retrieves outer syntax
+  commands according to the specified name patterns.
+
+  \end{description}
+*}
+
+
+subsubsection {* Examples *}
+
+text {* Some common diagnostic commands are retrieved like this
+  (according to usual naming conventions): *}
+
+help "print"
+help "find"
 
 
 section {* Lexical matters \label{sec:outer-lex} *}
 
 text {* The outer lexical syntax consists of three main categories of