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