--- a/doc-src/System/Thy/document/Basics.tex Sun May 31 15:07:03 2009 +0200
+++ b/doc-src/System/Thy/document/Basics.tex Sun May 31 15:27:19 2009 +0200
@@ -275,7 +275,6 @@
Usage: isabelle-process [OPTIONS] [INPUT] [OUTPUT]
Options are:
- -C tell ML system to copy output image
-I startup Isar interaction mode
-P startup Proof General interaction mode
-S secure mode -- disallow critical operations
@@ -337,10 +336,6 @@
maximally shared, resulting in up to \isa{{\isachardoublequote}{\isadigit{5}}{\isadigit{0}}{\isacharpercent}{\isachardoublequote}} less disk space
consumption.
- \medskip The \verb|-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 \verb|-e| option, arbitrary ML code may be
passed to the Isabelle session from the command line. Multiple
\verb|-e|'s are evaluated in the given order. Strange things