1.1 --- a/doc-src/HOL/logics-HOL.tex	Fri May 26 11:17:53 2000 +0200
     1.2 +++ b/doc-src/HOL/logics-HOL.tex	Fri May 26 11:18:06 2000 +0200
     1.3 @@ -7,8 +7,13 @@
     1.4  %%% to index constants:   \\tt \([a-zA-Z0-9][a-zA-Z0-9_]*\)     \\cdx{\1}  
     1.5  %%% to deverbify:         \\verb|\([^|]*\)|     \\ttindex{\1}  
     1.6  
     1.7 -\title{\includegraphics[scale=0.5]{isabelle_hol} \\[4ex] 
     1.8 -       Isabelle's Logics: HOL}
     1.9 +
    1.10 +\title{\includegraphics[scale=0.5]{isabelle_hol} \\[4ex]
    1.11 +  Isabelle's Logics: HOL%
    1.12 +  \thanks{The research has been funded by the EPSRC (grants GR/G53279,
    1.13 +    GR/H40570, GR/K57381, GR/K77051, GR/M75440), by ESPRIT (projects 3245:
    1.14 +    Logical Frameworks, and 6453: Types) and by the DFG Schwerpunktprogramm
    1.15 +    \emph{Deduktion}.}}
    1.16  
    1.17  \author{Tobias Nipkow\footnote
    1.18  {Institut f\"ur Informatik, Technische Universit\"at M\"unchen,
    1.19 @@ -18,9 +23,6 @@
    1.20  Markus Wenzel\footnote
    1.21  {Institut f\"ur Informatik, Technische Universit\"at M\"unchen,
    1.22   \texttt{wenzelm@in.tum.de}}}
    1.23 -%\thanks{The research has been funded by the EPSRC (grants
    1.24 -%          GR/G53279, GR/H40570, GR/K57381, GR/K77051), by ESPRIT project
    1.25 -%          6453: Types, and by the DFG Schwerpunktprogramm \emph{Deduktion}.}
    1.26  
    1.27  \newcommand\subcaption[1]{\par {\centering\normalsize\sc#1\par}\bigskip
    1.28    \hrule\bigskip}

     2.1 --- a/doc-src/Intro/intro.tex	Fri May 26 11:17:53 2000 +0200
     2.2 +++ b/doc-src/Intro/intro.tex	Fri May 26 11:18:06 2000 +0200
     2.3 @@ -103,15 +103,16 @@
     2.4  Tobias Nipkow contributed most of the section on defining theories.
     2.5  Stefan Berghofer and Sara Kalvala suggested improvements.
     2.6  
     2.7 -Tobias Nipkow has made immense contributions to Isabelle, including the
     2.8 -parser generator, type classes, and the simplifier.  Carsten Clasohm and
     2.9 -Markus Wenzel made major contributions; Sonia Mahjoub and Karin Nimmermann
    2.10 -also helped.  Isabelle was developed using Dave Matthews's Standard~{\sc
    2.11 -  ml} compiler, Poly/{\sc ml}.  Many people have contributed to Isabelle's
    2.12 -standard object-logics, including Martin Coen, Philippe de Groote, Philippe
    2.13 -No\"el.  The research has been funded by the EPSRC (grants
    2.14 -GR/G53279, GR/H40570, GR/K57381, GR/K77051)
    2.15 -and by ESPRIT (projects 3245: Logical Frameworks, and 6453: Types).
    2.16 +Tobias Nipkow has made immense contributions to Isabelle, including the parser
    2.17 +generator, type classes, and the simplifier.  Carsten Clasohm and Markus
    2.18 +Wenzel made major contributions; Sonia Mahjoub and Karin Nimmermann also
    2.19 +helped.  Isabelle was developed using Dave Matthews's Standard~{\sc ml}
    2.20 +compiler, Poly/{\sc ml}.  Many people have contributed to Isabelle's standard
    2.21 +object-logics, including Martin Coen, Philippe de Groote, Philippe No\"el.
    2.22 +The research has been funded by the EPSRC (grants GR/G53279, GR/H40570,
    2.23 +GR/K57381, GR/K77051, GR/M75440) and by ESPRIT (projects 3245: Logical
    2.24 +Frameworks, and 6453: Types), and by the DFG Schwerpunktprogramm
    2.25 +\emph{Deduktion}.
    2.26  
    2.27  \newpage
    2.28  \pagestyle{plain} \tableofcontents 

     3.1 --- a/doc-src/Logics/logics.tex	Fri May 26 11:17:53 2000 +0200
     3.2 +++ b/doc-src/Logics/logics.tex	Fri May 26 11:18:06 2000 +0200
     3.3 @@ -19,8 +19,9 @@
     3.4     wrote the first version of the logic~\LK{}.  Tobias Nipkow developed
     3.5     \LCF{} and~\Cube{}.  Martin Coen developed~\Modal{} with assistance
     3.6     from Rajeev Gor\'e.  The research has been funded by the EPSRC
     3.7 -   (grants GR/G53279, GR/H40570, GR/K57381, GR/K77051) and by ESPRIT
     3.8 -   project 6453: Types.} }
     3.9 +   (grants GR/G53279, GR/H40570, GR/K57381, GR/K77051, GR/M75440) and by ESPRIT
    3.10 +   (projects 3245: Logical Frameworks, and 6453: Types), and by the DFG
    3.11 +  Schwerpunktprogramm \emph{Deduktion}.} }
    3.12  
    3.13  \newcommand\subcaption[1]{\par {\centering\normalsize\sc#1\par}\bigskip
    3.14    \hrule\bigskip}

     4.1 --- a/doc-src/Ref/ref.tex	Fri May 26 11:17:53 2000 +0200
     4.2 +++ b/doc-src/Ref/ref.tex	Fri May 26 11:18:06 2000 +0200
     4.3 @@ -18,11 +18,12 @@
     4.4    and part of
     4.5    Chapter~\protect\ref{theories}.  Carsten Clasohm also contributed to
     4.6    Chapter~\protect\ref{theories}.  Markus Wenzel contributed to
     4.7 -  Chapter~\protect\ref{chap:syntax}.  Sara Kalvala, Martin Simons and others
     4.8 -  suggested changes
     4.9 +  Chapter~\protect\ref{chap:syntax}.  Jeremy Dawson, Sara Kalvala, Martin
    4.10 +  Simons  and others suggested changes
    4.11    and corrections.  The research has been funded by the EPSRC (grants
    4.12 -  GR/G53279, GR/H40570, GR/K57381, GR/K77051) and by ESPRIT project 6453:
    4.13 -  Types.}} 
    4.14 +  GR/G53279, GR/H40570, GR/K57381, GR/K77051, GR/M75440) and by ESPRIT
    4.15 +  (projects 3245: Logical Frameworks, and 6453: Types), and by the DFG
    4.16 +  Schwerpunktprogramm \emph{Deduktion}.}}  
    4.17  
    4.18  \makeindex
    4.19  

     5.1 --- a/doc-src/ZF/logics-ZF.tex	Fri May 26 11:17:53 2000 +0200
     5.2 +++ b/doc-src/ZF/logics-ZF.tex	Fri May 26 11:18:06 2000 +0200
     5.3 @@ -18,7 +18,9 @@
     5.4      Philippe de Groote contributed to~\ZF{}.  Philippe No\"el and
     5.5      Martin Coen made many contributions to~\ZF{}.  The research has 
     5.6      been funded by the EPSRC (grants GR/G53279, GR/H40570, GR/K57381,
     5.7 -    GR/K77051) and by ESPRIT project 6453: Types.}
     5.8 +    GR/K77051, GR/M75440) and by ESPRIT (projects 3245:
     5.9 +    Logical Frameworks, and 6453: Types) and by the DFG Schwerpunktprogramm
    5.10 +    \emph{Deduktion}.}
    5.11  }
    5.12  
    5.13  \newcommand\subcaption[1]{\par {\centering\normalsize\sc#1\par}\bigskip