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 \index{Wenzel, Markus}%
12 Another departure from previous documentation is that we describe Markus
13 Wenzel's proof script notation instead of ML tactic scripts. The latter
14 make it easier to introduce new tactics on the fly, but hardly anybody
15 does that. Wenzel's dedicated syntax is elegant, replacing for example
16 eight simplification tactics with a single method, namely \isa{simp},
17 with associated options.
19 \REMARK{mention Wenzel once author?}
20 The typesetting relies on Wenzel's theory presentation tools. An
21 annotated source file is run, typesetting the theory
22 % and any requested Isabelle responses
23 in the form of a \TeX\ source file. This book is
24 derived almost entirely from output generated in this way.
26 This tutorial owes a lot to the constant discussions with and the valuable
27 feedback from the Isabelle group at Munich: Stefan Berghofer, Olaf
28 M{\"u}ller, Wolfgang Naraschewski, David von Oheimb, Leonor Prensa Nieto,
29 Cornelia Pusch, Norbert Schirmer, Martin Strecker and Markus Wenzel. Stephan
30 Merz was also kind enough to read and comment on a draft version. We
31 received comments from Stefano Bistarelli, Gergely Buday and Tanja
32 Vos.\REMARK{incomplete list!}
34 The research has been funded by many sources, including the {\sc dfg} grants
35 Ni~491/2, Ni~491/3, Ni~491/4 and the {\sc epsrc} grants GR\slash K57381,
36 GR\slash K77051, GR\slash M75440, GR\slash R01156\slash 01 and by the
37 \textsc{esprit} working groups 21900 and IST-1999-29001 (the \emph{Types}