diff options
Diffstat (limited to 'doc')
| -rw-r--r-- | doc/refman/RefMan-tac.tex | 23 |
1 files changed, 15 insertions, 8 deletions
diff --git a/doc/refman/RefMan-tac.tex b/doc/refman/RefMan-tac.tex index a3953bb968..11568bb4d3 100644 --- a/doc/refman/RefMan-tac.tex +++ b/doc/refman/RefMan-tac.tex @@ -2680,14 +2680,6 @@ the same variants as {\tt rewrite} has. \end{Variants} - -\subsection{\tt cutrewrite -> \term$_1$ = \term$_2$} -\label{cutrewrite} -\tacindex{cutrewrite} - -This tactic acts like {\tt replace {\term$_1$} with {\term$_2$}} -(see below). - \subsection{\tt replace \term$_1$ with \term$_2$} \label{tactic:replace} \tacindex{replace \dots\ with} @@ -2738,6 +2730,21 @@ n}| assumption || symmetry; try assumption]}. in the conclusion of the goal. The \nterm{clause} argument must not contain any \texttt{type of} nor \texttt{value of}. +\item {\tt cutrewrite <- (\term$_1$ = \term$_2$)} +%\label{cutrewrite} +\tacindex{cutrewrite} + +This tactic is deprecated. It acts like {\tt replace {\term$_2$} with + {\term$_1$}}, or, equivalently as {\tt enough} (\term$_1$ = +\term$_2$) {\tt as <-}. + +\item {\tt cutrewrite -> (\term$_1$ = \term$_2$)} +%\label{cutrewrite} +\tacindex{cutrewrite} + +This tactic is deprecated. It can be replaced by {\tt enough} +(\term$_1$ = \term$_2$) {\tt as ->}. + \end{Variants} \subsection{\tt subst \ident} |