--- a/doc-src/System/basics.tex Thu Sep 28 14:47:42 2000 +0200
+++ b/doc-src/System/basics.tex Thu Sep 28 14:48:05 2000 +0200
@@ -213,6 +213,7 @@
Usage: isabelle [OPTIONS] [INPUT] [OUTPUT]
Options are:
+ -C tell ML system to copy output image
-I startup Isar interaction mode
-P startup Proof General interaction mode
-c tell ML system to compress output image
@@ -261,6 +262,10 @@
garbage collected and all values maximally shared, resulting in up to 50\%
less disk space consumption.
+\medskip The \texttt{-C} option tells the ML system to produce a completely
+self-contained output image, probably including a copy of the ML runtime
+system itself.
+
\medskip Using the \texttt{-e} option, arbitrary {\ML} code may be passed to
the Isabelle session from the command line. Multiple \texttt{-e}'s are
evaluated in the given order. Strange things may happen when errorneous {\ML}