post-CRC corrections
Tue, 03 May 1994 18:12:54 +0200
changeset 356 2e6545875982
parent 355 77150178beb2
child 357 a2c5cd25906e
post-CRC corrections
--- 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 @@
 \markboth{Preface}{Preface}   %or 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.
@@ -114,9 +114,10 @@
         host {\tt}\\
         directory {\tt local/lehrstuhl/nipkow}
-My electronic mail address is {\tt lcp\at}.  Please report any
-errors you find in this book and your problems or successes with Isabelle.
+The electronic distribution list {\tt isabelle-users\at}
+provides a forum for discussing problems and applications involving
+Isabelle.  To join, send me a message via {\tt lcp\at}.
+Please notify me of any errors you find in this book.
 Tobias Nipkow has made immense contributions to Isabelle, including the