# HG changeset patch
# User paulson
# Date 994857007 -7200
# Node ID 582433f7f6188be5497df816db10507284006716
# Parent  138919f1a135af5381fa4018764e122996fe5ccf
new preface

diff -r 138919f1a135 -r 582433f7f618 doc-src/TutorialI/preface.tex
--- /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).