\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.

Another departure from previous documentation is the use of Markus

Wenzel's proof script notation instead of ML tactic files.  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,

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 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).