diff -r 894d76cbf56d -r 802acc97fdaf doc-src/HOL/logics-HOL.tex
--- a/doc-src/HOL/logics-HOL.tex	Fri May 26 11:17:53 2000 +0200
+++ b/doc-src/HOL/logics-HOL.tex	Fri May 26 11:18:06 2000 +0200
@@ -7,8 +7,13 @@
 %%% to index constants:   \\tt \([a-zA-Z0-9][a-zA-Z0-9_]*\)     \\cdx{\1}  
 %%% to deverbify:         \\verb|\([^|]*\)|     \\ttindex{\1}  
 
-\title{\includegraphics[scale=0.5]{isabelle_hol} \\[4ex] 
-       Isabelle's Logics: HOL}
+
+\title{\includegraphics[scale=0.5]{isabelle_hol} \\[4ex]
+  Isabelle's Logics: HOL%
+  \thanks{The research has been funded by the EPSRC (grants GR/G53279,
+    GR/H40570, GR/K57381, GR/K77051, GR/M75440), by ESPRIT (projects 3245:
+    Logical Frameworks, and 6453: Types) and by the DFG Schwerpunktprogramm
+    \emph{Deduktion}.}}
 
 \author{Tobias Nipkow\footnote
 {Institut f\"ur Informatik, Technische Universit\"at M\"unchen,
@@ -18,9 +23,6 @@
 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}