Removed the \date{} command in order to put the date of typesetting on the
title page
--- a/doc-src/Intro/intro.tex Thu Apr 17 18:10:49 1997 +0200
+++ b/doc-src/Intro/intro.tex Thu Apr 17 18:16:12 1997 +0200
@@ -16,7 +16,6 @@
Computer Laboratory \\ University of Cambridge \\[2ex]
{\small{\em Electronic mail\/}: {\tt lcp@cl.cam.ac.uk}}
}
-\date{}
\makeindex
\underscoreoff
--- a/doc-src/Logics/logics.tex Thu Apr 17 18:10:49 1997 +0200
+++ b/doc-src/Logics/logics.tex Thu Apr 17 18:16:12 1997 +0200
@@ -29,8 +29,6 @@
{\small{\em Electronic mail\/}: {\tt lcp@cl.cam.ac.uk}} \\[3cm]
{\small Copyright \copyright{} \number\year{} by Lawrence C. Paulson} }
-\date{}
-
\newcommand\subcaption[1]{\par {\centering\normalsize\sc#1\par}\bigskip
\hrule\bigskip}
\newenvironment{constants}{\begin{center}\small\begin{tabular}{rrrr}}{\end{tabular}\end{center}}
--- a/doc-src/Ref/ref.tex Thu Apr 17 18:10:49 1997 +0200
+++ b/doc-src/Ref/ref.tex Thu Apr 17 18:16:12 1997 +0200
@@ -28,7 +28,6 @@
\small{\em Electronic mail\/}: {\tt lcp@cl.cam.ac.uk}\\[3cm]
Copyright \copyright{} \number\year{} by Lawrence C. Paulson}
-\date{}
\makeindex
\underscoreoff