diff options
| -rw-r--r-- | doc/RefMan-tac.tex | 4 |
1 files changed, 4 insertions, 0 deletions
diff --git a/doc/RefMan-tac.tex b/doc/RefMan-tac.tex index 1275134af6..33238d7f62 100644 --- a/doc/RefMan-tac.tex +++ b/doc/RefMan-tac.tex @@ -1337,6 +1337,10 @@ conditions that should hold for the instance $(I~\vec{t})$ to be proved by $c_i$. \begin{Variants} +\item \texttt{Inversion} \num\\ + This does the same thing as \texttt{Intros until \num} then +\texttt{Inversion \ident} where \ident is the identifier for the last +introduced hypothesis. \item \texttt{Inversion\_clear} \ident\\ \tacindex{Inversion\_clear} That does \texttt{Inversion} and then erases \ident~ from the |