1\chapter*{Preface}
2\markboth{Preface}{Preface}
3
4This volume is a self-contained introduction to interactive proof
5in higher-order logic (HOL), using the proof assistant Isabelle. 
6It is written for potential users rather
7than for our colleagues in the research world.
8
9The book has three parts.  
10\begin{itemize}
11\item 
12The first part, \textbf{Elementary Techniques},
13shows how to model functional programs in higher-order logic.  Early
14examples involve lists and the natural numbers.  Most proofs
15are two steps long, consisting of induction on a chosen variable
16followed by the \isa{auto} tactic.  But even this elementary part
17covers such advanced topics as nested and mutual recursion.
18\item 
19The second part, \textbf{Logic and Sets}, presents a collection of
20lower-level tactics that you can use to apply rules selectively.  It
21also describes Isabelle/HOL's treatment of sets, functions and
22relations and explains how to define sets inductively.  One of the
23examples concerns the theory of model checking, and another is drawn
24from a classic textbook on formal languages.
25\item 
26The third part, \textbf{Advanced Material}, describes a variety of other
27topics.  Among these are the real numbers, records and overloading.  Advanced
28techniques for induction and recursion are described.  A whole chapter is
29devoted to an extended example: the verification of a security protocol.
30\end{itemize}
31
32The typesetting relies on Wenzel's theory presentation tools.  An
33annotated source file is run, typesetting the theory
34in the form of a \LaTeX\ source file.  This book is derived almost entirely
35from output generated in this way.  The final chapter of Part~I explains how
36users may produce their own formal documents in a similar fashion.
37
38Isabelle's \hfootref{https://isabelle.in.tum.de/}{web site} contains
39links to the download area and to documentation and other information.
40The classic Isabelle user interface is Proof~General~/ Emacs by David
41Aspinall's\index{Aspinall, David}.  This book says very little about
42Proof General, which has its own documentation.
43
44This tutorial owes a lot to the constant discussions with and the valuable
45feedback from the Isabelle group at Munich: Stefan Berghofer, Olaf
46M{\"u}ller, Wolfgang Naraschewski, David von Oheimb, Leonor Prensa Nieto,
47Cornelia Pusch, Norbert Schirmer and Martin Strecker. Stephan
48Merz was also kind enough to read and comment on a draft version.  We
49received comments from Stefano Bistarelli, Gergely Buday, John Matthews
50and Tanja Vos.
51
52The research has been funded by many sources, including the {\sc dfg} grants
53NI~491/2, NI~491/3, NI~491/4, NI~491/6, {\sc bmbf} project Verisoft, the {\sc
54epsrc} grants GR/K57381, GR/K77051, GR/M75440, GR/R01156/01 GR/S57198/01 and
55by the \textsc{esprit} working groups 21900 and IST-1999-29001 (the
56\emph{Types} project).
57