--- a/doc-src/TutorialI/preface.tex Tue Aug 28 13:15:15 2012 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,56 +0,0 @@
-\chapter*{Preface}
-\markboth{Preface}{Preface}
-
-This volume is a self-contained introduction to interactive proof
-in higher-order logic (HOL), using the proof assistant Isabelle.
-It is written for potential users rather
-than for our colleagues in the research world.
-
-The book has three parts.
-\begin{itemize}
-\item
-The first part, \textbf{Elementary Techniques},
-shows how to model functional programs in higher-order logic. Early
-examples involve lists and the natural numbers. Most proofs
-are two steps long, consisting of induction on a chosen variable
-followed by the \isa{auto} tactic. But even this elementary part
-covers such advanced topics as nested and mutual recursion.
-\item
-The second part, \textbf{Logic and Sets}, presents a collection of
-lower-level tactics that you can use to apply rules selectively. It
-also describes Isabelle/HOL's treatment of sets, functions and
-relations and explains how to define sets inductively. One of the
-examples concerns the theory of model checking, and another is drawn
-from a classic textbook on formal languages.
-\item
-The third part, \textbf{Advanced Material}, describes a variety of other
-topics. Among these are the real numbers, records and overloading. Advanced
-techniques for induction and recursion are described. A whole chapter is
-devoted to an extended example: the verification of a security protocol.
-\end{itemize}
-
-The typesetting relies on Wenzel's theory presentation tools. An
-annotated source file is run, typesetting the theory
-in the form of a \LaTeX\ source file. This book is derived almost entirely
-from output generated in this way. The final chapter of Part~I explains how
-users may produce their own formal documents in a similar fashion.
-
-Isabelle's \hfootref{http://isabelle.in.tum.de/}{web site} contains
-links to the download area and to documentation and other information.
-The classic Isabelle user interface is Proof~General~/ Emacs by David
-Aspinall's\index{Aspinall, David}. This book says very little about
-Proof General, which has its own documentation.
-
-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 and Martin Strecker. Stephan
-Merz was also kind enough to read and comment on a draft version. We
-received comments from Stefano Bistarelli, Gergely Buday, John Matthews
-and Tanja Vos.
-
-The research has been funded by many sources, including the {\sc dfg} grants
-NI~491/2, NI~491/3, NI~491/4, NI~491/6, {\sc bmbf} project Verisoft, the {\sc
-epsrc} grants GR/K57381, GR/K77051, GR/M75440, GR/R01156/01 GR/S57198/01 and
-by the \textsc{esprit} working groups 21900 and IST-1999-29001 (the
-\emph{Types} project).