--- a/doc-src/IsarRef/intro.tex Fri Mar 17 22:50:41 2000 +0100
+++ b/doc-src/IsarRef/intro.tex Fri Mar 17 22:51:05 2000 +0100
@@ -3,6 +3,8 @@
\section{Quick start}
+\subsection{Terminal sessions}
+
Isar is already part of Isabelle (as of version Isabelle99, or later). The
\texttt{isabelle} binary provides option \texttt{-I} to run the Isar
interaction loop at startup, rather than the plain ML top-level. Thus the
@@ -18,59 +20,66 @@
Note that any Isabelle/Isar command may be retracted by \texttt{undo}; the
\texttt{help} command prints a list of available language elements.
-Plain TTY-based interaction like this used to be quite feasible with
+
+\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
-demands some better user-interface support. \emph{Proof~General}\index{Proof
- General} of LFCS Edinburgh \cite{proofgeneral} offers a generic Emacs-based
-environment for interactive theorem provers that does all the cut-and-paste
-and forward-backward walk through the text in a very neat way. Note that in
-Isabelle/Isar, the current position within a partial proof document is equally
-important than the actual proof state. Thus Proof~General provides the
-canonical working environment for Isabelle/Isar, both for getting acquainted
-(e.g.\ by replaying existing Isar documents) and real production work.
+demands some better user-interface support. David Aspinall's
+\emph{Proof~General}\index{Proof General} environment
+\cite{proofgeneral,Aspinall:TACAS:2000} offers a generic Emacs-based interface
+for interactive theorem provers that does all the cut-and-paste and
+forward-backward walk through the text in a very neat way. In Isabelle/Isar,
+the current position within a partial proof document is equally important than
+the actual proof state. Thus Proof~General provides the canonical working
+environment for Isabelle/Isar, both for getting acquainted (e.g.\ by replaying
+existing Isar documents) and real production work.
\medskip
The easiest way to use Proof~General is to make it the default Isabelle user
-interface. Just put something like this into your Isabelle settings file (see
-also \cite{isabelle-sys}):
+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="-u false"
+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.} 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)
+ classic Isabelle tactic scripts.}
- Starts Proof General for Isabelle/Isar with proof documents FILES
- (default Scratch.thy).
+%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} %$
- PROOFGENERAL_OPTIONS=
-\end{ttbox} %$
-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 may be configured as follows:
-\begin{ttbox}
-PROOFGENERAL_OPTIONS="-u false -p emacs"
-\end{ttbox}
+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
-proper startup may be still achieved by using the \texttt{-u false}
-option.\footnote{Any Emacs lisp file \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.}
+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
+automatically loaded by the Proof~General interface script as well.
\medskip
@@ -80,9 +89,17 @@
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}
-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,Aspinall:TACAS:2000} for further basic command sequences,
+such as ``\texttt{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.
\section{Isabelle/Isar theories}
@@ -94,7 +111,7 @@
\item A \emph{formal proof document language} designed to support intelligible
semi-automated reasoning. Instead of putting together unreadable tactic
scripts, the author is enabled to express the reasoning in way that is close
- to mathematical practice.
+ to usual mathematical practice.
\end{enumerate}
The Isar proof language is embedded into the new theory format as a proper
@@ -146,12 +163,13 @@
\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/Isar/} \\
\end{tabular}
\end{center}
See \texttt{HOL/Isar_examples} for a collection of introductory examples, and
\texttt{HOL/HOL-Real/HahnBanach} is a big mathematics application. Apart from
-browsable HTML sources, both sessions provide actual documents (in PDF).
+plain HTML sources, these sessions also provide actual documents (in PDF).
%%% Local Variables:
%%% mode: latex