1.1 --- a/doc-src/IsarRef/intro.tex	Wed Aug 04 18:20:05 1999 +0200
     1.2 +++ b/doc-src/IsarRef/intro.tex	Wed Aug 04 18:20:24 1999 +0200
     1.3 @@ -3,12 +3,79 @@
     1.4  
     1.5  \section{Quick start}
     1.6  
     1.7 -FIXME examples, ProofGeneral setup
     1.8 +Isar is already part of Isabelle (as of version Isabelle99, or later).  The
     1.9 +\texttt{isabelle} binary provides option \texttt{-I} to run the Isar
    1.10 +interaction loop at startup, rather than the plain ML top-level.  Thus the
    1.11 +quickest way to do anything with Isabelle/Isar is as follows:
    1.12 +\begin{ttbox}
    1.13 +isabelle -I HOL\medskip
    1.14 +\out{> Welcome to Isabelle/HOL (Isabelle99)}\medskip
    1.15 +theory Foo = Main:
    1.16 +constdefs foo :: nat  "foo == 1"
    1.17 +lemma "0 < foo" by (simp add: foo_def)
    1.18 +end
    1.19 +\end{ttbox}
    1.20  
    1.21 -\section{Examples}
    1.22 +Plain TTY-based interaction like this used to be quite feasible with
    1.23 +traditional tactic based theorem proving, but developing Isar documents
    1.24 +demands some better user-interface support.
    1.25 +\emph{ProofGeneral}\index{ProofGeneral} of LFCS Edinburgh \cite{proofgeneral}
    1.26 +offers a generic Emacs-based environment for interactive theorem provers that
    1.27 +does all the cut-and-paste and forward-backward walk through the document in a
    1.28 +very neat way.  Note that in Isabelle/Isar, the current position within a
    1.29 +partial proof document is more informative than the actual proof state.  Thus
    1.30 +the ProofGeneral/isar interface provides the canonical working environment for
    1.31 +Isabelle/Isar, both for getting acquainted (e.g.\ by replaying existing Isar
    1.32 +documents) and serious production work.
    1.33 +
    1.34 +\medskip
    1.35 +
    1.36 +The easiest way to use ProofGeneral/isar is to make it the default Isabelle
    1.37 +user interface.  Just say something like this in your Isabelle settings file
    1.38 +(cf.\ \cite{isabelle-sys}):
    1.39 +\begin{ttbox}
    1.40 +ISABELLE_INTERFACE=\$ISABELLE_HOME/contrib/ProofGeneral/isar/interface
    1.41 +PROOFGENERAL_OPTIONS=""
    1.42 +\end{ttbox}
    1.43 +You may have to change \texttt{\$ISABELLE_HOME/contrib/ProofGeneral} to the
    1.44 +actual installation directory of ProofGeneral.  Now the capital
    1.45 +\texttt{Isabelle} binary refers to the ProofGeneral/isar interface.  It's
    1.46 +usage is as follows:
    1.47 +\begin{ttbox}
    1.48 +Usage: interface [OPTIONS] [FILES ...]
    1.49 +
    1.50 +Options are:
    1.51 +  -l NAME      logic image name (default $ISABELLE_LOGIC=HOL)
    1.52 +  -p NAME      Emacs program name (default xemacs)
    1.53 +  -u BOOL      use .emacs file (default false)
    1.54 +  -w BOOL      use window system (default true)
    1.55 +
    1.56 +Starts ProofGeneral for Isabelle/Isar with proof documents FILES
    1.57 +(default Scratch.thy).
    1.58 +\end{ttbox}
    1.59 +The defaults for these options may be changed via the
    1.60 +\texttt{PROOFGENERAL_OPTIONS} setting.  For example, GNU Emacs with loading of
    1.61 +the startup file enabled may be configured as follows:\footnote{The interface
    1.62 +  disables \texttt{.emacs} by default to ensure successful startup despite any
    1.63 +  strange commands that tend to occur there.}
    1.64 +\begin{ttbox}
    1.65 +PROOFGENERAL_OPTIONS="-p emacs -u true"
    1.66 +\end{ttbox}
    1.67 +
    1.68 +With the proper Isabelle interface setup, Isar documents may now be edited by
    1.69 +visiting appropriate theory files, e.g.\ 
    1.70 +\begin{ttbox}
    1.71 +Isabelle \({\langle}isabellehome{\rangle}\)/src/HOL/Isar_examples/BasicLogic.thy
    1.72 +\end{ttbox}
    1.73 +Users of XEmacs may note the toolbar for navigating forward and backward
    1.74 +through the text.  Consult the ProofGeneral documentation for further basic
    1.75 +commands, such as \texttt{c-c return} or \texttt{c-c u}.
    1.76 +
    1.77  
    1.78  \section{How to write Isar proofs anyway?}
    1.79  
    1.80 +FIXME
    1.81 +
    1.82  
    1.83  %%% Local Variables: 
    1.84  %%% mode: latex