diff -r 77150178beb2 -r 2e6545875982 doc-src/preface.tex
--- 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