1.1 --- a/doc-src/TutorialI/preface.tex	Tue Dec 18 16:14:50 2001 +0100
     1.2 +++ b/doc-src/TutorialI/preface.tex	Tue Dec 18 16:14:56 2001 +0100
     1.3 @@ -1,10 +1,11 @@
     1.4  \chapter*{Preface}
     1.5  \markboth{Preface}{Preface}
     1.6  
     1.7 -This volume is a self-contained introduction to interactive proof using
     1.8 -Isabelle/HOL\@.  Compared with existing Isabelle documentation, it
     1.9 -provides a straightforward route into higher-order logic, which most
    1.10 -people prefer these days. It bypasses first-order logic and minimizes
    1.11 +This volume is a self-contained introduction to interactive proof
    1.12 +in higher-order logic (HOL), using the proof assistant Isabelle/HOL\@. 
    1.13 +Compared with existing Isabelle documentation,
    1.14 +it provides a direct route into higher-order logic, which most people
    1.15 +prefer these days. It bypasses first-order logic and minimizes
    1.16  discussion of meta-theory.  It is written for potential users rather
    1.17  than for our colleagues in the research world.
    1.18  
    1.19 @@ -16,20 +17,56 @@
    1.20  eight simplification tactics with a single method, namely \isa{simp},
    1.21  with associated options.
    1.22  
    1.23 -\REMARK{mention Wenzel once author?}
    1.24 +The book has three parts.  
    1.25 +\begin{itemize}
    1.26 +\item 
    1.27 +The first part, \textbf{Basic Techniques},
    1.28 +shows how to model functional programs in higher-order logic.  Early
    1.29 +examples involve lists and the natural numbers.  Most proofs
    1.30 +are two steps long, consisting of induction on a chosen variable
    1.31 +followed by the \isa{auto} tactic.  But even this elementary part
    1.32 +covers such advanced topics as nested and mutual recursion.
    1.33 +\item 
    1.34 +The second part, \textbf{Logic and Sets}, presents a collection of
    1.35 +lower-level tactics that you can use to apply rules selectively.  It
    1.36 +also describes Isabelle/HOL's treatment of sets, functions and
    1.37 +relations and explains how to define sets inductively.  One of the
    1.38 +examples concerns the theory of model checking, and another is drawn
    1.39 +from a classic textbook on formal languages.
    1.40 +\item 
    1.41 +The third part, \textbf{Advanced Material}, describes a variety of
    1.42 +other topics.  Among these are the real numbers, records and
    1.43 +overloading.  Esoteric techniques are described involving induction and
    1.44 +recursion.  A whole chapter is devoted to an extended example: the
    1.45 +verification of a security protocol.
    1.46 +\end{itemize}
    1.47 +
    1.48  The typesetting relies on Wenzel's theory presentation tools.  An
    1.49  annotated source file is run, typesetting the theory
    1.50  % and any requested Isabelle responses
    1.51  in the form of a \TeX\ source file.  This book is
    1.52  derived almost entirely from output generated in this way.
    1.53  
    1.54 +Isabelle's
    1.55 +\href{http://www.cl.cam.ac.uk/Research/HVG/Isabelle/}{web site}
    1.56 +contains links to the download area and to documentation and other
    1.57 +information.  Most Isabelle sessions are now run from within David
    1.58 +Aspinall's wonderful user interface,
    1.59 +\href{http://www.proofgeneral.org/}{Proof General}.  This book says
    1.60 +very little about Proof General, which has its own documentation.  In
    1.61 +order to run Isabelle, you will need a Standard ML compiler.  We
    1.62 +recommend \href{http://www.polyml.org/}{Poly/ML}, which is free and
    1.63 +gives the best performance.  The other supported compiler is
    1.64 +\href{http://cm.bell-labs.com/cm/cs/what/smlnj/index.html}{Standard
    1.65 +ML of New Jersey}.
    1.66 +
    1.67  This tutorial owes a lot to the constant discussions with and the valuable
    1.68  feedback from the Isabelle group at Munich: Stefan Berghofer, Olaf
    1.69  M{\"u}ller, Wolfgang Naraschewski, David von Oheimb, Leonor Prensa Nieto,
    1.70  Cornelia Pusch, Norbert Schirmer, Martin Strecker and Markus Wenzel. Stephan
    1.71  Merz was also kind enough to read and comment on a draft version.  We
    1.72  received comments from Stefano Bistarelli, Gergely Buday and Tanja
    1.73 -Vos.\REMARK{incomplete list!}
    1.74 +Vos.
    1.75  
    1.76  The research has been funded by many sources, including the {\sc dfg} grants
    1.77  Ni~491/2, Ni~491/3, Ni~491/4 and the {\sc epsrc} grants GR\slash K57381,