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