isabelle -C;
Thu, 28 Sep 2000 14:48:05 +0200
changeset 10108 72a719e997b9
parent 10107 6715b2ce44d4
child 10109 dcb72400bc32
isabelle -C;
--- 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}