improved X-Symbol stuff;
Tue, 09 May 2000 14:16:32 +0200
changeset 8843 5370a030dd47
parent 8842 b90d653bd089
child 8844 db71c334e854
improved X-Symbol stuff;
--- 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}
 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.
+\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}''.
+\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:
+mkdir -p ~/.xemacs
+cd ~/.xemacs
+tar xzf .../x-symbol-pkg.tar.gz
+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