# HG changeset patch
# User nipkow
# Date 925981981 -7200
# Node ID c2754409919b40bc2515bfd60a50903bf495c1d0
# Parent  d646567156c3e4b2547b68182feed18f8c0920f1
New title page.

diff -r d646567156c3 -r c2754409919b doc-src/HOL/logics-HOL.tex
--- a/doc-src/HOL/logics-HOL.tex	Wed May 05 18:48:32 1999 +0200
+++ b/doc-src/HOL/logics-HOL.tex	Thu May 06 11:13:01 1999 +0200
@@ -17,14 +17,17 @@
 \title{\includegraphics[scale=0.5]{isabelle_hol.eps} \\[4ex] 
        Isabelle's Logics: HOL}
 
-\author{{\em Lawrence C. Paulson}\\
-        Computer Laboratory \\ University of Cambridge \\
-        \texttt{lcp@cl.cam.ac.uk}\\[3ex] 
-        With Contributions by Tobias Nipkow and Markus Wenzel%
-        \thanks{Tobias Nipkow developed~\HOL{}.  Markus Wenzel made numerous
-          improvements.  The research has been funded by the EPSRC (grants
-          GR/G53279, GR/H40570, GR/K57381, GR/K77051) and by ESPRIT project
-          6453: Types.}}
+\author{Tobias Nipkow\footnote
+{Institut f\"ur Informatik, Technische Universit\"at M\"unchen,
+ \texttt{nipkow@in.tum.de}},
+Lawrence C. Paulson\footnote
+{Computer Laboratory, University of Cambridge, \texttt{lcp@cl.cam.ac.uk}},
+Markus Wenzel\footnote
+{Institut f\"ur Informatik, Technische Universit\"at M\"unchen,
+ \texttt{wenzelm@in.tum.de}}}
+%\thanks{The research has been funded by the EPSRC (grants
+%          GR/G53279, GR/H40570, GR/K57381, GR/K77051), by ESPRIT project
+%          6453: Types, and by the DFG Schwerpunktprogramm \emph{Deduktion}.}
 
 \newcommand\subcaption[1]{\par {\centering\normalsize\sc#1\par}\bigskip
   \hrule\bigskip}