--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/TutorialI/preface.tex Wed Jul 11 15:10:07 2001 +0200
@@ -0,0 +1,33 @@
+\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).