--- a/doc-src/preface.tex Tue May 03 18:07:41 1994 +0200
+++ b/doc-src/preface.tex Tue May 03 18:12:54 1994 +0200
@@ -1,6 +1,6 @@
\chapter*{Preface}
\markboth{Preface}{Preface} %or Preface ?
-\addcontentsline{toc}{chapter}{Preface}
+%%\addcontentsline{toc}{chapter}{Preface}
Most theorem provers support a fixed logic, such as first-order or
equational logic. They bring sophisticated proof procedures to bear upon
@@ -48,8 +48,8 @@
These include first-order logic (intuitionistic and classical), the sequent
calculus, higher-order logic, Zermelo-Fraenkel set theory~\cite{suppes72},
a version of Constructive Type Theory~\cite{nordstrom90}, several modal
-logics, and a Logic for Computable Functions. Several experimental logics
-are being developed, such as linear logic.
+logics, and a Logic for Computable Functions~\cite{paulson87}. Several
+experimental logics are being developed, such as linear logic.
\centerline{\epsfbox{Isa-logics.eps}}
@@ -114,9 +114,10 @@
host {\tt ftp.informatik.tu-muenchen.de}\\
directory {\tt local/lehrstuhl/nipkow}
\end{itemize}
-My electronic mail address is {\tt lcp\at cl.cam.ac.uk}. Please report any
-errors you find in this book and your problems or successes with Isabelle.
-
+The electronic distribution list {\tt isabelle-users\at cl.cam.ac.uk}
+provides a forum for discussing problems and applications involving
+Isabelle. To join, send me a message via {\tt lcp\at cl.cam.ac.uk}.
+Please notify me of any errors you find in this book.
\section*{Acknowledgements}
Tobias Nipkow has made immense contributions to Isabelle, including the