- Runs <command>elim H hyps</command>, clears H and tries to run
- itself recursively on each new identifier introduced by
- <command>elim</command> in the opened sequents.
+ Runs <command>
+ elim H H<subscript>1</subscript> ... H<subscript>m</subscript>
+ </command>, clears <command>H</command> and tries to run itself
+ recursively on each new identifier introduced by
+ <command>elim</command> in the opened sequents.
+ If <command>H</command> is not provided tries this operation on
+ each premise in the current context.