diff options
| -rw-r--r-- | doc/refman/RefMan-tac.tex | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/doc/refman/RefMan-tac.tex b/doc/refman/RefMan-tac.tex index 656ae57b95..54393e46f6 100644 --- a/doc/refman/RefMan-tac.tex +++ b/doc/refman/RefMan-tac.tex @@ -1278,7 +1278,7 @@ in the list of subgoals remaining to prove. In particular, \texttt{pose proof {\term} as {\ident}} behaves as \texttt{assert ({\ident} := {\term})} and \texttt{pose proof {\term} - as {\intropattern}\tacindex{pose proof}} is the same as applying + as {\intropattern}} is the same as applying the {\intropattern} to {\term}. \item \texttt{enough ({\ident} :\ {\form})}\tacindex{enough} |