2 \markboth{Preface}{Preface}
4 This volume is a self-contained introduction to interactive proof using
5 Isabelle/HOL\@. Compared with existing Isabelle documentation, it
6 provides a straightforward route into higher-order logic, which most
7 people prefer these days. It bypasses first-order logic and minimizes
8 discussion of meta-theory. It is written for potential users rather
9 than for our colleagues in the research world.
11 Another departure from previous documentation is the use of Markus
12 Wenzel's proof script notation instead of ML tactic files. The latter
13 make it easier to introduce new tactics on the fly, but hardly anybody
14 does that. Wenzel's dedicated syntax is elegant, replacing for example
15 eight simplification tactics with a single method, namely \isa{simp},
16 with associated options.
18 The typesetting relies on Wenzel's proof presentation tools. A possibly
19 annotated theory file is run, typesetting the theory and any requested
20 Isabelle responses in the form of a \TeX{} source file. This book is
21 derived almost entirely from output generated in this way.
23 This tutorial owes a lot to the constant discussions with and the valuable
24 feedback from the Isabelle group at Munich: Stefan Berghofer, Olaf M{\"u}ller,
25 Wolfgang Naraschewski, David von Oheimb, Leonor Prensa Nieto, Cornelia Pusch,
26 Martin Strecker and Markus Wenzel. Stephan Merz was also kind enough to
27 read and comment on a draft version. We received comments from Stefano
28 Bistarelli, Gergely Buday and Tanja Vos.\REMARK{incomplete list!}
30 The research has been funded by many sources, including the {\sc epsrc}
31 grants GR\slash K57381, GR\slash K77051,
32 GR\slash M75440, GR\slash R01156\slash 01 and by the \textsc{esprit}
33 working groups 21900 and IST-1999-29001 (the \emph{Types} project).