diff options
author | 2017-05-03 10:23:46 +0200 | |
---|---|---|
committer | 2017-05-03 10:23:46 +0200 | |
commit | 4a84961049f4f00897ae72a13954edbcc9aaba5e (patch) | |
tree | 00b0a1fb7cf66d4bf6fd096e23fc177ed38a7b95 /doc | |
parent | 510701319b1b0420698e411e24022a0fbec7c36c (diff) |
Fix outdated description in RefMan.
Diffstat (limited to 'doc')
-rw-r--r-- | doc/refman/RefMan-pro.tex | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/doc/refman/RefMan-pro.tex b/doc/refman/RefMan-pro.tex index c37367de5..4c333379b 100644 --- a/doc/refman/RefMan-pro.tex +++ b/doc/refman/RefMan-pro.tex @@ -118,7 +118,7 @@ the current proof and declare the initial goal as an axiom. \subsection[\tt Proof {\term}.]{\tt Proof {\term}.\comindex{Proof} \label{BeginProof}} This command applies in proof editing mode. It is equivalent to {\tt - exact {\term}; Save.} That is, you have to give the full proof in + exact {\term}. Qed.} That is, you have to give the full proof in one gulp, as a proof term (see Section~\ref{exact}). \variant {\tt Proof.} |