# HG changeset patch
# User wenzelm
# Date 1124356654 -7200
# Node ID 3016fd89574f403722a79ae391fe56f9cb4d9daf
# Parent  dd769bd4d056daea9e5fcac70a943ed48d5e3cf7
usedir: tuned option -V;

diff -r dd769bd4d056 -r 3016fd89574f doc-src/System/present.tex
--- a/doc-src/System/present.tex	Thu Aug 18 11:17:33 2005 +0200
+++ b/doc-src/System/present.tex	Thu Aug 18 11:17:34 2005 +0200
@@ -424,14 +424,16 @@
 \texttt{document} directory.  See \S\ref{sec:tool-document} and
 \S\ref{sec:tool-latex} for more details.
 
-\medskip The \texttt{-V} option (which may be repeated) declares alternative
-document versions, consisting of name/tags pairs (cf.\ options \texttt{-n} and
-\texttt{-t} of the \texttt{document} tool, \S\ref{sec:tool-document}).  The
-standard document is equivalent to ``\texttt{document=theory,proof,ML}'',
-which means that all theory begin/end commands, proof body texts, and ML code
-will be presented faithfully.  An alternative version
-``\texttt{outline=/proof/ML}'' would fold proof and ML parts, replacing the
-original text by a short place-holder.
+\medskip The \texttt{-V} option declares alternative document versions,
+consisting of name/tags pairs (cf.\ options \texttt{-n} and \texttt{-t} of the
+\texttt{document} tool, \S\ref{sec:tool-document}).  The standard document is
+equivalent to ``\texttt{document=theory,proof,ML}'', which means that all
+theory begin/end commands, proof body texts, and ML code will be presented
+faithfully.  An alternative version ``\texttt{outline=/proof/ML}'' would fold
+proof and ML parts, replacing the original text by a short place-holder.  The
+form ``$name$\verb,=-,'' means to remove document $name$ from the list of
+versions to be processed.  Any number of \texttt{-V} options may be given;
+later declarations have precedence over earlier ones.
 
 \medskip The \texttt{-g} option produces images of the theory dependency graph
 (cf.\ \S\ref{sec:browse}) for inclusion in the generated document, both as