# HG changeset patch
# User wenzelm
# Date 953403002 -3600
# Node ID f5f6a97ee43fc0a1cdabe82baa8c82d5e017c941
# Parent  160739e1f44350ecd2f5b376dc5420347c86e255
simplified setup;
tuned;

diff -r 160739e1f443 -r f5f6a97ee43f doc-src/IsarRef/intro.tex
--- a/doc-src/IsarRef/intro.tex	Sat Mar 18 19:07:47 2000 +0100
+++ b/doc-src/IsarRef/intro.tex	Sat Mar 18 19:10:02 2000 +0100
@@ -50,32 +50,14 @@
 interface.\footnote{There is also a \texttt{ProofGeneral/isa} interface, for
   classic Isabelle tactic scripts.}
 
-%FIXME remove?
-%Its usage is as follows:
-%\begin{ttbox}
-%Usage: interface [OPTIONS] [FILES ...]
-%
-%  Options are:
-%    -l NAME      logic image name (default $ISABELLE_LOGIC=HOL)
-%    -p NAME      Emacs program name (default xemacs)
-%    -u BOOL      use .emacs file (default true)
-%    -w BOOL      use window system (default true)
-%    -x BOOL      enable x-symbol package
-%  Starts Proof General for Isabelle/Isar with proof documents FILES
-%  (default Scratch.thy).
-%
-%  PROOFGENERAL_OPTIONS=
-%\end{ttbox} %$
+The interface script provides several options, just pass ``\texttt{-?}'' 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"}.
 
-The interface script provides several options (pass ``\texttt{-?}'' 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 GNU Emacs instead of XEmacs (which is the default) may be
-configured in Isabelle's settings via \texttt{PROOFGENERAL_OPTIONS="-p
-  emacs"}.
-
-Occasionally, a user's \texttt{.emacs} file contains material that is
-incompatible with the version of (X)Emacs that Proof~General prefers.  Then
+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 \texttt{proofgeneral-settings.el} occurring
 in \texttt{\$ISABELLE_HOME/etc} or \texttt{\$ISABELLE_HOME_USER/etc} is
@@ -89,22 +71,29 @@
 Isabelle \({\langle}isabellehome{\rangle}\)/src/HOL/Isar_examples/BasicLogic.thy
 \end{ttbox}
 Users of XEmacs may note the tool bar for navigating forward and backward
-through the text.  Consult the Proof~General documentation
-\cite{proofgeneral,Aspinall:TACAS:2000} for further basic command sequences,
-such as ``\texttt{c-c return}'' or ``\texttt{c-c u}''.
+through the text.  Consult the Proof~General documentation \cite{proofgeneral}
+for further basic command sequences, such as ``\texttt{c-c c-return}'' or
+``\texttt{c-c u}''.
 
 \medskip
 
 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.
 Just pass option \texttt{-x true} to the Isabelle interface script, or check
-the appropriate menu setting by hand.  In any case, the X-Symbol package
-already must have been properly installed.
+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~/X-Symbol.
 
 
 \section{Isabelle/Isar theories}
 
-Isabelle/Isar offers two main improvements over classic Isabelle:
+Isabelle/Isar offers the following main improvements over classic Isabelle:
 \begin{enumerate}
 \item A new \emph{theory format}, occasionally referred to as ``new-style
   theories'', supporting interactive development and unlimited undo operation.
@@ -112,6 +101,10 @@
   semi-automated reasoning.  Instead of putting together unreadable tactic
   scripts, the author is enabled to express the reasoning in way that is close
   to usual mathematical practice.
+\item A simple document preparation system for Isabelle/Isar theories, for
+  typesetting formal developments together with informal text.  The resulting
+  resulting hyper-linked PDF documents are equally well suited for WWW
+  presentation and printed copies.
 \end{enumerate}
 
 The Isar proof language is embedded into the new theory format as a proper
@@ -158,11 +151,12 @@
 give some clues of how the concepts introduced here may be put into practice.
 Appendix~\ref{ap:refcard} provides a quick reference card of the most common
 Isabelle/Isar language elements.  There are several examples distributed with
-Isabelle, and available via the Isabelle WWW library:
+Isabelle, and available via the Isabelle WWW library as well as the
+Isabelle/Isar page:
 \begin{center}\small
   \begin{tabular}{l}
     \url{http://www.cl.cam.ac.uk/Research/HVG/Isabelle/library/} \\
-    \url{http://isabelle.in.tum.de/library/} \\
+    \url{http://isabelle.in.tum.de/library/} \\[1ex]
     \url{http://isabelle.in.tum.de/Isar/} \\
   \end{tabular}
 \end{center}