--- a/doc-src/System/Thy/Basics.thy Tue Sep 16 17:16:27 2008 +0200
+++ b/doc-src/System/Thy/Basics.thy Tue Sep 16 17:16:28 2008 +0200
@@ -511,9 +511,7 @@
proper setup of the Proof General Lisp packages. There are some
options available, such as @{verbatim "-l"} for passing the logic
image to be used by default, or @{verbatim "-m"} to tune the
- standard print mode. The @{verbatim "-I"} option allows to switch
- between the Isar and ML view, independently of the interface script
- being used.
+ standard print mode.
\medskip Note that the world may be also seen the other way round:
Emacs may be started first (with proper setup of Proof General