1.1 --- a/doc-src/IsarRef/basics.tex	Thu Aug 19 19:56:17 1999 +0200
     1.2 +++ b/doc-src/IsarRef/basics.tex	Thu Aug 19 20:05:13 1999 +0200
     1.3 @@ -1,11 +1,39 @@
     1.4  
     1.5 -\chapter{Basic Concepts}
     1.6 +\chapter{Basic Concepts}\label{ch:basics}
     1.7  
     1.8 -\section{Isabelle/Isar Theories}
     1.9 +Isabelle/Isar offers two main improvements over classic Isabelle:
    1.10 +\begin{enumerate}
    1.11 +\item A new \emph{theory format}, often referred to as ``new-style theories'',
    1.12 +  supporting interactive development with unlimited undo operation.
    1.13 +\item A formal \emph{proof language} language designed to support
    1.14 +  \emph{intelligible} semi-automated reasoning.  Rather than putting together
    1.15 +  tactic scripts, the author is enabled to express the reasoning in way that
    1.16 +  is close to mathematical practice.
    1.17 +\end{enumerate}
    1.18 +
    1.19 +The Isar proof language is embedded into the new theory format as a proper
    1.20 +sub-language.  Proof mode is entered by stating some $\THEOREMNAME$ or
    1.21 +$\LEMMANAME$ at the theory levels, and left with the final end of proof.  Some
    1.22 +theory extension mechanisms require proof as well, such as the HOL
    1.23 +$\isarkeyword{typedef}$.
    1.24 +
    1.25 +New-style theory files may still be associated with an ML file consisting of
    1.26 +plain old tactic scripts.  Generally, migration between the two formats is
    1.27 +made relatively easy, and users may start to benefit from interactive theory
    1.28 +development even before they have any idea of the Isar proof language.
    1.29 +
    1.30  
    1.31  \section{The Isar proof language}
    1.32  
    1.33 -\subsection{Proof commands}
    1.34 +This rather important section has not been written yet!  Refer to
    1.35 +\cite{Wenzel:1999:TPHOL} for the time being.
    1.36 +
    1.37 +\subsection{Commands}
    1.38 +
    1.39 +\subsubsection{Isar primitives}
    1.40 +
    1.41 +\subsubsection{Derived elements}
    1.42 +
    1.43  
    1.44  \subsection{Methods}
    1.45  

     2.1 --- a/doc-src/IsarRef/intro.tex	Thu Aug 19 19:56:17 1999 +0200
     2.2 +++ b/doc-src/IsarRef/intro.tex	Thu Aug 19 20:05:13 1999 +0200
     2.3 @@ -11,36 +11,36 @@
     2.4  isabelle -I HOL\medskip
     2.5  \out{> Welcome to Isabelle/HOL (Isabelle99)}\medskip
     2.6  theory Foo = Main:
     2.7 -constdefs foo :: nat  "foo == 1"
     2.8 -lemma "0 < foo" by (simp add: foo_def)
     2.9 +constdefs foo :: nat  "foo == 1";
    2.10 +lemma "0 < foo" by (simp add: foo_def);
    2.11  end
    2.12  \end{ttbox}
    2.13 +Note that \emph{any} Isabelle/Isar command may be retracted by \texttt{undo}.
    2.14  
    2.15  Plain TTY-based interaction like this used to be quite feasible with
    2.16  traditional tactic based theorem proving, but developing Isar documents
    2.17 -demands some better user-interface support.
    2.18 -\emph{ProofGeneral}\index{ProofGeneral} of LFCS Edinburgh \cite{proofgeneral}
    2.19 -offers a generic Emacs-based environment for interactive theorem provers that
    2.20 -does all the cut-and-paste and forward-backward walk through the document in a
    2.21 -very neat way.  Note that in Isabelle/Isar, the current position within a
    2.22 -partial proof document is more informative than the actual proof state.  Thus
    2.23 -the ProofGeneral/isar interface provides the canonical working environment for
    2.24 -Isabelle/Isar, both for getting acquainted (e.g.\ by replaying existing Isar
    2.25 -documents) and serious production work.
    2.26 +demands some better user-interface support.  \emph{Proof~General}\index{Proof
    2.27 +  General} of LFCS Edinburgh \cite{proofgeneral} offers a generic Emacs-based
    2.28 +environment for interactive theorem provers that does all the cut-and-paste
    2.29 +and forward-backward walk through the document in a very neat way.  Note that
    2.30 +in Isabelle/Isar, the current position within a partial proof document is more
    2.31 +informative than the actual proof state.  Thus Proof~General provides the
    2.32 +canonical working environment for Isabelle/Isar, both for getting acquainted
    2.33 +(e.g.\ by replaying existing Isar documents) and serious production work.
    2.34  
    2.35  \medskip
    2.36  
    2.37 -The easiest way to use ProofGeneral/isar is to make it the default Isabelle
    2.38 -user interface.  Just say something like this in your Isabelle settings file
    2.39 -(cf.\ \cite{isabelle-sys}):
    2.40 +The easiest way to use ProofGeneral is to make it the default Isabelle user
    2.41 +interface.  Just say something like this in your Isabelle settings file (cf.\ 
    2.42 +\cite{isabelle-sys}):
    2.43  \begin{ttbox}
    2.44  ISABELLE_INTERFACE=\$ISABELLE_HOME/contrib/ProofGeneral/isar/interface
    2.45  PROOFGENERAL_OPTIONS=""
    2.46  \end{ttbox}
    2.47  You may have to change \texttt{\$ISABELLE_HOME/contrib/ProofGeneral} to the
    2.48 -actual installation directory of ProofGeneral.  Now the capital
    2.49 -\texttt{Isabelle} binary refers to the ProofGeneral/isar interface.  It's
    2.50 -usage is as follows:
    2.51 +actual installation directory of Proof~General.  Now the capital
    2.52 +\texttt{Isabelle} binary refers to the \texttt{ProofGeneral/isar} interface.
    2.53 +It's usage is as follows:
    2.54  \begin{ttbox}
    2.55  Usage: interface [OPTIONS] [FILES ...]
    2.56  
    2.57 @@ -50,14 +50,15 @@
    2.58    -u BOOL      use .emacs file (default false)
    2.59    -w BOOL      use window system (default true)
    2.60  
    2.61 -Starts ProofGeneral for Isabelle/Isar with proof documents FILES
    2.62 +Starts Proof General for Isabelle/Isar with proof documents FILES
    2.63  (default Scratch.thy).
    2.64  \end{ttbox}
    2.65  The defaults for these options may be changed via the
    2.66 -\texttt{PROOFGENERAL_OPTIONS} setting.  For example, GNU Emacs with loading of
    2.67 -the startup file enabled may be configured as follows:\footnote{The interface
    2.68 -  disables \texttt{.emacs} by default to ensure successful startup despite any
    2.69 -  strange commands that tend to occur there.}
    2.70 +\texttt{PROOFGENERAL_OPTIONS} setting.  For example, GNU Emacs\footnote{GNU
    2.71 +  Emacs version 20.x required.} with loading of the startup file enabled may
    2.72 +be configured as follows:\footnote{The interface disables \texttt{.emacs} by
    2.73 +  default to ensure successful startup despite any strange commands that tend
    2.74 +  to occur there.}
    2.75  \begin{ttbox}
    2.76  PROOFGENERAL_OPTIONS="-p emacs -u true"
    2.77  \end{ttbox}
    2.78 @@ -68,13 +69,28 @@
    2.79  Isabelle \({\langle}isabellehome{\rangle}\)/src/HOL/Isar_examples/BasicLogic.thy
    2.80  \end{ttbox}
    2.81  Users of XEmacs may note the toolbar for navigating forward and backward
    2.82 -through the text.  Consult the ProofGeneral documentation for further basic
    2.83 -commands, such as \texttt{c-c return} or \texttt{c-c u}.
    2.84 +through the text.  Consult the Proof~General documentation \cite{proofgeneral}
    2.85 +for further basic commands, such as \texttt{c-c return} or \texttt{c-c u}.
    2.86  
    2.87  
    2.88  \section{How to write Isar proofs anyway?}
    2.89  
    2.90 -FIXME
    2.91 +This is one of the key questions, of course.  Isar offers a rather different
    2.92 +approach to formal proof documents than plain old tactic scripts.  Experienced
    2.93 +users of existing interactive theorem proving systems may have to learn
    2.94 +thinking different in order to make effective use of Isabelle/Isar.  On the
    2.95 +other hand, Isabelle/Isar comes much closer to existing mathematical practice
    2.96 +of formal proof, so users with less experience in old-style tactical proving,
    2.97 +but a good understanding of mathematical proof might cope with Isar even
    2.98 +better.
    2.99 +
   2.100 +Unfortunately, there is no tutorial on Isabelle/Isar available yet.  This
   2.101 +document really is a \emph{reference manual}.  Nevertheless, we will give some
   2.102 +discussions of the general principles underlying Isar in
   2.103 +chapter~\ref{ch:basics}, and provide some clues of how these may be put into
   2.104 +practice.  Some more background information on Isar is given in
   2.105 +\cite{Wenzel:1999:TPHOL}.  Furthermore, there are several examples distributed
   2.106 +with Isabelle (see directory \texttt{HOL/Isar_examples}).
   2.107  
   2.108  
   2.109  %%% Local Variables: 

     3.1 --- a/doc-src/IsarRef/isar-ref.tex	Thu Aug 19 19:56:17 1999 +0200
     3.2 +++ b/doc-src/IsarRef/isar-ref.tex	Thu Aug 19 20:05:13 1999 +0200
     3.3 @@ -56,7 +56,7 @@
     3.4    Any of the Isabelle/Isar commands may be executed in single-steps, so
     3.5    basically the interpreter has a proof text debugger already built-in.
     3.6    
     3.7 -  Employing the \emph{ProofGeneral/isar} instantiation of the generic Emacs
     3.8 +  Employing the Isar instantiation of \emph{Proof~General}, the generic Emacs
     3.9    interface for interactive proof assistants of LFCS Edinburgh, we arrive at a
    3.10    reasonable environment for \emph{live document editing}.  Thus proof texts
    3.11    may be developed incrementally by issuing proper document constructors,