+ [&sterm;… | <emphasis role="bold">_</emphasis>]]
+ </entry>
+ <entry>The natural number, which defaults to 1, gives a bound to
+ the depth of the search tree. The terms listed is the only
+ knowledge base used by automation together with all indexed factual
+ and equational theorems in the included library. If the list of terms
+ is empty, only equational theorems and facts in the library are
+ used. If the list is omitted, it defaults to all indexed theorems
+ in the library. Finally, if the list is <command>_</command>,
+ the automation command becomes a macro that is expanded in a new
+ automation command where <command>_</command> is replaced with the
+ list of theorems required to prove the sequent.