# HG changeset patch
# User wenzelm
# Date 957874592 -7200
# Node ID 5370a030dd471521e046828a411a7e01a3073837
# Parent  b90d653bd089b9fe9f6cca628a953649aabdd663
improved X-Symbol stuff;

diff -r b90d653bd089 -r 5370a030dd47 doc-src/IsarRef/intro.tex
--- a/doc-src/IsarRef/intro.tex	Tue May 09 11:29:13 2000 +0200
+++ b/doc-src/IsarRef/intro.tex	Tue May 09 14:16:32 2000 +0200
@@ -21,7 +21,7 @@
 \texttt{help} command prints a list of available language elements.
 
 
-\subsection{The Proof~General interface}
+\subsection{Proof~General}
 
 Plain TTY-based interaction as above used to be quite feasible with
 traditional tactic based theorem proving, but developing Isar documents really
@@ -35,7 +35,8 @@
 environment for Isabelle/Isar, both for getting acquainted (e.g.\ by replaying
 existing Isar documents) and for production work.
 
-\medskip
+
+\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
@@ -75,7 +76,8 @@
 for further basic command sequences, such as ``\texttt{C-c C-return}'' or
 ``\texttt{C-c u}''.
 
-\medskip
+
+\subsubsection{The X-Symbol package}
 
 Proof~General also supports the Emacs X-Symbol package \cite{x-symbol}, which
 provides a nice way to get proper mathematical symbols displayed on screen.
@@ -83,12 +85,26 @@
 the appropriate menu setting by hand.  In any case, the X-Symbol package must
 have been properly installed already.
 
-Note that using actual mathematical symbols in the text easily makes the ASCII
-sources hard to read.  For example, $\forall$ will appear as \verb,\\<forall>,
-according the default set of Isabelle symbols.  On the other hand, the
-Isabelle document preparation system \cite{isabelle-sys} 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.
+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}
+
+\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.
 
 
 \section{Isabelle/Isar theories}
@@ -136,7 +152,7 @@
 emerging Isabelle/Isar document.
 
 
-\subsection{Document preparation}
+\subsection{Document preparation}\label{sec:document-prep}
 
 Isabelle/Isar provides a simple document preparation system based on current
 (PDF) {\LaTeX} technology, with full support of hyper-links (both local