1.1 --- a/doc-src/IsarRef/intro.tex Fri Mar 17 22:50:41 2000 +0100
1.2 +++ b/doc-src/IsarRef/intro.tex Fri Mar 17 22:51:05 2000 +0100
1.3 @@ -3,6 +3,8 @@
1.4
1.5 \section{Quick start}
1.6
1.7 +\subsection{Terminal sessions}
1.8 +
1.9 Isar is already part of Isabelle (as of version Isabelle99, or later). The
1.10 \texttt{isabelle} binary provides option \texttt{-I} to run the Isar
1.11 interaction loop at startup, rather than the plain ML top-level. Thus the
1.12 @@ -18,59 +20,66 @@
1.13 Note that any Isabelle/Isar command may be retracted by \texttt{undo}; the
1.14 \texttt{help} command prints a list of available language elements.
1.15
1.16 -Plain TTY-based interaction like this used to be quite feasible with
1.17 +
1.18 +\subsection{The Proof~General interface}
1.19 +
1.20 +Plain TTY-based interaction as above used to be quite feasible with
1.21 traditional tactic based theorem proving, but developing Isar documents
1.22 -demands some better user-interface support. \emph{Proof~General}\index{Proof
1.23 - General} of LFCS Edinburgh \cite{proofgeneral} offers a generic Emacs-based
1.24 -environment for interactive theorem provers that does all the cut-and-paste
1.25 -and forward-backward walk through the text in a very neat way. Note that in
1.26 -Isabelle/Isar, the current position within a partial proof document is equally
1.27 -important than the actual proof state. Thus Proof~General provides the
1.28 -canonical working environment for Isabelle/Isar, both for getting acquainted
1.29 -(e.g.\ by replaying existing Isar documents) and real production work.
1.30 +demands some better user-interface support. David Aspinall's
1.31 +\emph{Proof~General}\index{Proof General} environment
1.32 +\cite{proofgeneral,Aspinall:TACAS:2000} offers a generic Emacs-based interface
1.33 +for interactive theorem provers that does all the cut-and-paste and
1.34 +forward-backward walk through the text in a very neat way. In Isabelle/Isar,
1.35 +the current position within a partial proof document is equally important than
1.36 +the actual proof state. Thus Proof~General provides the canonical working
1.37 +environment for Isabelle/Isar, both for getting acquainted (e.g.\ by replaying
1.38 +existing Isar documents) and real production work.
1.39
1.40 \medskip
1.41
1.42 The easiest way to use Proof~General is to make it the default Isabelle user
1.43 -interface. Just put something like this into your Isabelle settings file (see
1.44 -also \cite{isabelle-sys}):
1.45 +interface (see also \cite{isabelle-sys}). Just put something like this into
1.46 +your Isabelle settings file:
1.47 \begin{ttbox}
1.48 ISABELLE_INTERFACE=\$ISABELLE_HOME/contrib/ProofGeneral/isar/interface
1.49 -PROOFGENERAL_OPTIONS="-u false"
1.50 +PROOFGENERAL_OPTIONS=""
1.51 \end{ttbox}
1.52 You may have to change \texttt{\$ISABELLE_HOME/contrib/ProofGeneral} to the
1.53 actual installation directory of Proof~General. From now on, the capital
1.54 \texttt{Isabelle} executable refers to the \texttt{ProofGeneral/isar}
1.55 interface.\footnote{There is also a \texttt{ProofGeneral/isa} interface, for
1.56 - classic Isabelle tactic scripts.} Its usage is as follows:
1.57 -\begin{ttbox}
1.58 -Usage: interface [OPTIONS] [FILES ...]
1.59 + classic Isabelle tactic scripts.}
1.60
1.61 - Options are:
1.62 - -l NAME logic image name (default $ISABELLE_LOGIC=HOL)
1.63 - -p NAME Emacs program name (default xemacs)
1.64 - -u BOOL use .emacs file (default true)
1.65 - -w BOOL use window system (default true)
1.66 +%FIXME remove?
1.67 +%Its usage is as follows:
1.68 +%\begin{ttbox}
1.69 +%Usage: interface [OPTIONS] [FILES ...]
1.70 +%
1.71 +% Options are:
1.72 +% -l NAME logic image name (default $ISABELLE_LOGIC=HOL)
1.73 +% -p NAME Emacs program name (default xemacs)
1.74 +% -u BOOL use .emacs file (default true)
1.75 +% -w BOOL use window system (default true)
1.76 +% -x BOOL enable x-symbol package
1.77 +% Starts Proof General for Isabelle/Isar with proof documents FILES
1.78 +% (default Scratch.thy).
1.79 +%
1.80 +% PROOFGENERAL_OPTIONS=
1.81 +%\end{ttbox} %$
1.82
1.83 - Starts Proof General for Isabelle/Isar with proof documents FILES
1.84 - (default Scratch.thy).
1.85 -
1.86 - PROOFGENERAL_OPTIONS=
1.87 -\end{ttbox} %$
1.88 -Apart from the command line, the defaults for these options may be overridden
1.89 -via the \texttt{PROOFGENERAL_OPTIONS} setting as well. For example, plain GNU
1.90 -Emacs may be configured as follows:
1.91 -\begin{ttbox}
1.92 -PROOFGENERAL_OPTIONS="-u false -p emacs"
1.93 -\end{ttbox}
1.94 +The interface script provides several options (pass ``\texttt{-?}'' to see its
1.95 +usage). Apart from the command line, the defaults for these options may be
1.96 +overridden via the \texttt{PROOFGENERAL_OPTIONS} setting as well. For
1.97 +example, plain GNU Emacs instead of XEmacs (which is the default) may be
1.98 +configured in Isabelle's settings via \texttt{PROOFGENERAL_OPTIONS="-p
1.99 + emacs"}.
1.100
1.101 Occasionally, a user's \texttt{.emacs} file contains material that is
1.102 incompatible with the version of (X)Emacs that Proof~General prefers. Then
1.103 -proper startup may be still achieved by using the \texttt{-u false}
1.104 -option.\footnote{Any Emacs lisp file \texttt{proofgeneral-settings.el}
1.105 - occurring in \texttt{\$ISABELLE_HOME/etc} or
1.106 - \texttt{\$ISABELLE_HOME_USER/etc} is automatically loaded by the
1.107 - Proof~General interface script as well.}
1.108 +proper startup may be still achieved by using the \texttt{-u false} option.
1.109 +Also note that any Emacs lisp file \texttt{proofgeneral-settings.el} occurring
1.110 +in \texttt{\$ISABELLE_HOME/etc} or \texttt{\$ISABELLE_HOME_USER/etc} is
1.111 +automatically loaded by the Proof~General interface script as well.
1.112
1.113 \medskip
1.114
1.115 @@ -80,9 +89,17 @@
1.116 Isabelle \({\langle}isabellehome{\rangle}\)/src/HOL/Isar_examples/BasicLogic.thy
1.117 \end{ttbox}
1.118 Users of XEmacs may note the tool bar for navigating forward and backward
1.119 -through the text. Consult the Proof~General documentation \cite{proofgeneral}
1.120 -for further basic command sequences, such as ``\texttt{c-c return}'' or
1.121 -``\texttt{c-c u}''.
1.122 +through the text. Consult the Proof~General documentation
1.123 +\cite{proofgeneral,Aspinall:TACAS:2000} for further basic command sequences,
1.124 +such as ``\texttt{c-c return}'' or ``\texttt{c-c u}''.
1.125 +
1.126 +\medskip
1.127 +
1.128 +Proof~General also supports the Emacs X-Symbol package \cite{x-symbol}, which
1.129 +provides a nice way to get proper mathematical symbols displayed on screen.
1.130 +Just pass option \texttt{-x true} to the Isabelle interface script, or check
1.131 +the appropriate menu setting by hand. In any case, the X-Symbol package
1.132 +already must have been properly installed.
1.133
1.134
1.135 \section{Isabelle/Isar theories}
1.136 @@ -94,7 +111,7 @@
1.137 \item A \emph{formal proof document language} designed to support intelligible
1.138 semi-automated reasoning. Instead of putting together unreadable tactic
1.139 scripts, the author is enabled to express the reasoning in way that is close
1.140 - to mathematical practice.
1.141 + to usual mathematical practice.
1.142 \end{enumerate}
1.143
1.144 The Isar proof language is embedded into the new theory format as a proper
1.145 @@ -146,12 +163,13 @@
1.146 \begin{tabular}{l}
1.147 \url{http://www.cl.cam.ac.uk/Research/HVG/Isabelle/library/} \\
1.148 \url{http://isabelle.in.tum.de/library/} \\
1.149 + \url{http://isabelle.in.tum.de/Isar/} \\
1.150 \end{tabular}
1.151 \end{center}
1.152
1.153 See \texttt{HOL/Isar_examples} for a collection of introductory examples, and
1.154 \texttt{HOL/HOL-Real/HahnBanach} is a big mathematics application. Apart from
1.155 -browsable HTML sources, both sessions provide actual documents (in PDF).
1.156 +plain HTML sources, these sessions also provide actual documents (in PDF).
1.157
1.158 %%% Local Variables:
1.159 %%% mode: latex