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