diff options
Diffstat (limited to 'doc/refman/RefMan-pro.tex')
| -rw-r--r-- | doc/refman/RefMan-pro.tex | 19 |
1 files changed, 6 insertions, 13 deletions
diff --git a/doc/refman/RefMan-pro.tex b/doc/refman/RefMan-pro.tex index 739ca6b5..8c1a7824 100644 --- a/doc/refman/RefMan-pro.tex +++ b/doc/refman/RefMan-pro.tex @@ -163,28 +163,21 @@ as a {\tt Theorem}, the name {\ident} is known at all section levels: current section. \end{Variants} -\subsection{\tt Proof {\term}.}\comindex{Proof} +\subsection{\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 one gulp, as a proof term (see section \ref{exact}). -\begin{Variants} - -\item{\tt Proof.} +\variant {\tt Proof.} Is a noop which is useful to delimit the sequence of tactic commands which start a proof, after a {\tt Theorem} command. It is a good practice to use {\tt Proof.} as an opening parenthesis, closed in the script with a closing {\tt Qed.} -\item{\tt Proof with {\tac}.} - - This command may be used to start a proof. It defines a default - tactic to be used each time a tactic command is ended by - ``\verb#...#''. In this case the tactic command typed by the user is - equivalent to \emph{command};{\tac}. - -\end{Variants} +\SeeAlso {\tt Proof with {\tac}.} in section~\ref{ProofWith}. \subsection{\tt Abort.} \comindex{Abort} @@ -381,7 +374,7 @@ All the hypotheses remains usable in the proof development. This command goes back to the default mode which is to print all available hypotheses. -% $Id: RefMan-pro.tex 8609 2006-02-24 13:32:57Z notin,no-port-forwarding,no-agent-forwarding,no-X11-forwarding,no-pty $ +% $Id: RefMan-pro.tex 9030 2006-07-07 15:37:23Z herbelin $ %%% Local Variables: %%% mode: latex |