--- a/doc-src/System/Thy/Presentation.thy Sun Mar 20 17:40:45 2011 +0100
+++ b/doc-src/System/Thy/Presentation.thy Sun Mar 20 18:09:32 2011 +0100
@@ -448,7 +448,7 @@
-P PATH set path for remote theory browsing information
-Q INT set threshold for sub-proof parallelization (default 50)
-T LEVEL multithreading: trace level (default 0)
- -V VERSION declare alternative document VERSION
+ -V VARIANT declare alternative document VARIANT
-b build mode (output heap image, using current dir)
-d FORMAT build document as FORMAT (default false)
-f NAME use ML file NAME (default ROOT.ML)
@@ -523,16 +523,16 @@
\secref{sec:tool-latex} for more details.
\medskip The @{verbatim "-V"} option declares alternative document
- versions, consisting of name/tags pairs (cf.\ options @{verbatim
+ variants, consisting of name/tags pairs (cf.\ options @{verbatim
"-n"} and @{verbatim "-t"} of the @{tool_ref document} tool). The
standard document is equivalent to ``@{verbatim
"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 ``@{verbatim
+ faithfully. An alternative variant ``@{verbatim
"outline=/proof/ML"}'' would fold proof and ML parts, replacing the
original text by a short place-holder. The form ``@{text
name}@{verbatim "=-"},'' means to remove document @{text name} from
- the list of versions to be processed. Any number of @{verbatim
+ the list of variants to be processed. Any number of @{verbatim
"-V"} options may be given; later declarations have precedence over
earlier ones.