--- a/doc-src/System/Thy/document/Basics.tex Tue Sep 16 17:16:27 2008 +0200
+++ b/doc-src/System/Thy/document/Basics.tex Tue Sep 16 17:16:28 2008 +0200
@@ -522,9 +522,7 @@
proper setup of the Proof General Lisp packages. There are some
options available, such as \verb|-l| for passing the logic
image to be used by default, or \verb|-m| to tune the
- standard print mode. The \verb|-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