# HG changeset patch
# User wenzelm
# Date 968172309 -7200
# Node ID 71ad08ad2cf02c43441a554af989df930ec7d14c
# Parent  afc54ca6dc6f2147d97d5ec5e805f771c5c1fbbb
simplified PG/X-Symbol intro;

diff -r afc54ca6dc6f -r 71ad08ad2cf0 doc-src/IsarRef/intro.tex
--- a/doc-src/IsarRef/intro.tex	Tue Sep 05 18:44:42 2000 +0200
+++ b/doc-src/IsarRef/intro.tex	Tue Sep 05 18:45:09 2000 +0200
@@ -39,33 +39,15 @@
 
 \subsubsection{Proof~General as default Isabelle interface}
 
-The easiest way to use Proof~General is to make it the default Isabelle user
-interface (see also \cite{isabelle-sys}).  Just put something like this into
-your Isabelle settings file:
-\begin{ttbox}
-ISABELLE_INTERFACE=\$ISABELLE_HOME/contrib/ProofGeneral/isar/interface
-PROOFGENERAL_OPTIONS=""
-\end{ttbox}
-You may have to change \texttt{\$ISABELLE_HOME/contrib/ProofGeneral} to the
-actual installation directory of Proof~General.  From now on, the capital
-\texttt{Isabelle} executable refers to the \texttt{ProofGeneral/isar}
-interface.\footnote{There is also a \texttt{ProofGeneral/isa} interface, for
-  classic Isabelle tactic scripts.}
-
-The interface script provides several options, just pass \verb,-?, to see its
-usage.  Apart from the command line, the defaults for these options may be
-overridden via the \texttt{PROOFGENERAL_OPTIONS} setting as well.  For
-example, plain FSF Emacs (instead of the default XEmacs) may be configured in
-Isabelle's settings via \texttt{PROOFGENERAL_OPTIONS="-p emacs"}.
-
-Occasionally, the user's \verb,~/.emacs, file contains material that is
-incompatible with the version of Emacs that Proof~General prefers.  Then
-proper startup may be still achieved by using the \texttt{-u false} option.
-Also note that any Emacs lisp file called \texttt{proofgeneral-settings.el}
-occurring in \texttt{\$ISABELLE_HOME/etc} or \texttt{\$ISABELLE_HOME_USER/etc}
-is automatically loaded by the Proof~General interface script as well.
-
-\medskip
+The easiest way to invoke Proof~General is via the Isabelle interface wrapper
+script.  The default configuration of Isabelle is smart enough to detect the
+Proof~General distribution in several canonical places (e.g.\ 
+\texttt{\$ISABELLE_HOME/contrib/ProofGeneral}).  Thus the capital
+\texttt{Isabelle} executable would already refer to the
+\texttt{ProofGeneral/isar} interface without further ado.\footnote{There is
+  also a \texttt{ProofGeneral/isa} interface for old tactic scripts written in
+  ML.} The Isabelle interface script provides several options, just pass
+\verb,-?, to see its usage.
 
 With the proper Isabelle interface setup, Isar documents may now be edited by
 visiting appropriate theory files, e.g.\ 
@@ -77,6 +59,33 @@
 for further basic command sequences, such as ``\texttt{C-c C-return}'' or
 ``\texttt{C-c u}''.
 
+\medskip
+
+Proof~General may be also configured manually by giving Isabelle settings like
+this (see also \cite{isabelle-sys}):
+\begin{ttbox}
+ISABELLE_INTERFACE=\$ISABELLE_HOME/contrib/ProofGeneral/isar/interface
+PROOFGENERAL_OPTIONS=""
+\end{ttbox}
+You may have to change \texttt{\$ISABELLE_HOME/contrib/ProofGeneral} to the
+actual installation directory of Proof~General.
+
+\medskip
+
+Apart from the Isabelle command line, defaults for interface options may be
+given by the \texttt{PROOFGENERAL_OPTIONS} setting as well.  For example, the
+Emacs executable to be used may be configured in Isabelle's settings like this:
+\begin{ttbox}
+PROOFGENERAL_OPTIONS="-p xemacs-nomule"  
+\end{ttbox}
+
+Occasionally, the user's \verb,~/.emacs, file contains material that is
+incompatible with the version of Emacs that Proof~General prefers.  Then
+proper startup may be still achieved by using the \texttt{-u false} option.
+Also note that any Emacs lisp file called \texttt{proofgeneral-settings.el}
+occurring in \texttt{\$ISABELLE_HOME/etc} or \texttt{\$ISABELLE_HOME_USER/etc}
+is automatically loaded by the Proof~General interface script as well.
+
 
 \subsubsection{The X-Symbol package}
 
@@ -87,24 +96,21 @@
 have been properly installed already.
 
 Contrary to what you may expect from the documentation of X-Symbol, the
-package is very easy to install for individual users and configures itself
-automatically.  Simply download the ``binary'' package file, and do something
-like this to install it in your home directory:
-\begin{ttbox}
-mkdir -p ~/.xemacs
-cd ~/.xemacs
-tar xzf .../x-symbol-pkg.tar.gz
-\end{ttbox}
+package is very easy to install and configures itself automatically.  The
+default configuration of Isabelle is smart enough to detect the X-Symbol
+package in several canonical places (e.g.\ 
+\texttt{\$ISABELLE_HOME/contrib/x-symbol}).
 
 \medskip
 
 Using proper mathematical symbols in Isabelle theories can be very convenient
 for readability of large formulas.  On the other hand, the plain ASCII sources
-easily become somewhat unintelligible.  For example, $\forall$ will appear as
-\verb,\<forall>, according the default set of Isabelle symbols.  Nevertheless,
-the Isabelle document preparation system (see \S\ref{sec:document-prep}) will
-be happy to print non-ASCII symbols properly.  It is even possible to invent
-additional notation beyond the display capabilities of XEmacs and X-Symbol.
+easily become somewhat unintelligible.  For example, $\Longrightarrow$ will
+appear as \verb,\<Longrightarrow>, according the default set of Isabelle
+symbols.  Nevertheless, the Isabelle document preparation system (see
+\S\ref{sec:document-prep}) will be happy to print non-ASCII symbols properly.
+It is even possible to invent additional notation beyond the display
+capabilities of XEmacs and X-Symbol.
 
 
 \section{Isabelle/Isar theories}