--- a/doc-src/System/Thy/document/Basics.tex Sun May 31 15:29:43 2009 +0200
+++ b/doc-src/System/Thy/document/Basics.tex Sun May 31 15:49:35 2009 +0200
@@ -280,7 +280,6 @@
-S secure mode -- disallow critical operations
-W OUTPUT startup process wrapper, with messages going to OUTPUT stream
-X startup PGIP interaction mode
- -c tell ML system to compress output image
-e MLTEXT pass MLTEXT to the ML session
-f pass 'Session.finish();' to the ML session
-m MODE add print mode for output
@@ -330,12 +329,6 @@
read-only after terminating. Thus subsequent invocations cause the
logic image to be read-only automatically.
- \medskip The \verb|-c| option tells the underlying ML system
- to compress the output heap (fully transparently). On Poly/ML for
- example, the image is garbage collected and all stored values are
- maximally shared, resulting in up to \isa{{\isachardoublequote}{\isadigit{5}}{\isadigit{0}}{\isacharpercent}{\isachardoublequote}} less disk space
- consumption.
-
\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