--- 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}