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