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

\REMARK{mention Wenzel once author?}

The typesetting relies on Wenzel's theory presentation tools.  An

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