# HG changeset patch
# User wenzelm
# Date 1221578188 -7200
# Node ID e2f5bf4994988fe03dfc62586d34fb90405ba013
# Parent  5440452371e985cadf0bda4ca283cb9bbe4acda6
Proof General: option -I is obsolete;

diff -r 5440452371e9 -r e2f5bf499498 doc-src/System/Thy/Basics.thy
--- 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
diff -r 5440452371e9 -r e2f5bf499498 doc-src/System/Thy/document/Basics.tex
--- 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