# HG changeset patch
# User paulson
# Date 959332686 -7200
# Node ID 802acc97fdaf528f8cbe7e65e691e62a164630f0
# Parent  894d76cbf56db11c0eb188fd274c3265db3f81b4
updated acknowledgements

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}
diff -r 894d76cbf56d -r 802acc97fdaf doc-src/Intro/intro.tex
--- a/doc-src/Intro/intro.tex	Fri May 26 11:17:53 2000 +0200
+++ b/doc-src/Intro/intro.tex	Fri May 26 11:18:06 2000 +0200
@@ -103,15 +103,16 @@
 Tobias Nipkow contributed most of the section on defining theories.
 Stefan Berghofer and Sara Kalvala suggested improvements.
 
-Tobias Nipkow has made immense contributions to Isabelle, including the
-parser generator, type classes, and the simplifier.  Carsten Clasohm and
-Markus Wenzel made major contributions; Sonia Mahjoub and Karin Nimmermann
-also helped.  Isabelle was developed using Dave Matthews's Standard~{\sc
-  ml} compiler, Poly/{\sc ml}.  Many people have contributed to Isabelle's
-standard object-logics, including Martin Coen, Philippe de Groote, Philippe
-No\"el.  The research has been funded by the EPSRC (grants
-GR/G53279, GR/H40570, GR/K57381, GR/K77051)
-and by ESPRIT (projects 3245: Logical Frameworks, and 6453: Types).
+Tobias Nipkow has made immense contributions to Isabelle, including the parser
+generator, type classes, and the simplifier.  Carsten Clasohm and Markus
+Wenzel made major contributions; Sonia Mahjoub and Karin Nimmermann also
+helped.  Isabelle was developed using Dave Matthews's Standard~{\sc ml}
+compiler, Poly/{\sc ml}.  Many people have contributed to Isabelle's standard
+object-logics, including Martin Coen, Philippe de Groote, Philippe No\"el.
+The research has been funded by the EPSRC (grants GR/G53279, GR/H40570,
+GR/K57381, GR/K77051, GR/M75440) and by ESPRIT (projects 3245: Logical
+Frameworks, and 6453: Types), and by the DFG Schwerpunktprogramm
+\emph{Deduktion}.
 
 \newpage
 \pagestyle{plain} \tableofcontents 
diff -r 894d76cbf56d -r 802acc97fdaf doc-src/Logics/logics.tex
--- a/doc-src/Logics/logics.tex	Fri May 26 11:17:53 2000 +0200
+++ b/doc-src/Logics/logics.tex	Fri May 26 11:18:06 2000 +0200
@@ -19,8 +19,9 @@
    wrote the first version of the logic~\LK{}.  Tobias Nipkow developed
    \LCF{} and~\Cube{}.  Martin Coen developed~\Modal{} with assistance
    from Rajeev Gor\'e.  The research has been funded by the EPSRC
-   (grants GR/G53279, GR/H40570, GR/K57381, GR/K77051) and by ESPRIT
-   project 6453: Types.} }
+   (grants GR/G53279, GR/H40570, GR/K57381, GR/K77051, GR/M75440) and by ESPRIT
+   (projects 3245: Logical Frameworks, and 6453: Types), and by the DFG
+  Schwerpunktprogramm \emph{Deduktion}.} }
 
 \newcommand\subcaption[1]{\par {\centering\normalsize\sc#1\par}\bigskip
   \hrule\bigskip}
diff -r 894d76cbf56d -r 802acc97fdaf doc-src/Ref/ref.tex
--- a/doc-src/Ref/ref.tex	Fri May 26 11:17:53 2000 +0200
+++ b/doc-src/Ref/ref.tex	Fri May 26 11:18:06 2000 +0200
@@ -18,11 +18,12 @@
   and part of
   Chapter~\protect\ref{theories}.  Carsten Clasohm also contributed to
   Chapter~\protect\ref{theories}.  Markus Wenzel contributed to
-  Chapter~\protect\ref{chap:syntax}.  Sara Kalvala, Martin Simons and others
-  suggested changes
+  Chapter~\protect\ref{chap:syntax}.  Jeremy Dawson, Sara Kalvala, Martin
+  Simons  and others suggested changes
   and corrections.  The research has been funded by the EPSRC (grants
-  GR/G53279, GR/H40570, GR/K57381, GR/K77051) and by ESPRIT project 6453:
-  Types.}} 
+  GR/G53279, GR/H40570, GR/K57381, GR/K77051, GR/M75440) and by ESPRIT
+  (projects 3245: Logical Frameworks, and 6453: Types), and by the DFG
+  Schwerpunktprogramm \emph{Deduktion}.}}  
 
 \makeindex
 
diff -r 894d76cbf56d -r 802acc97fdaf doc-src/ZF/logics-ZF.tex
--- a/doc-src/ZF/logics-ZF.tex	Fri May 26 11:17:53 2000 +0200
+++ b/doc-src/ZF/logics-ZF.tex	Fri May 26 11:18:06 2000 +0200
@@ -18,7 +18,9 @@
     Philippe de Groote contributed to~\ZF{}.  Philippe No\"el and
     Martin Coen made many contributions to~\ZF{}.  The research has 
     been funded by the EPSRC (grants GR/G53279, GR/H40570, GR/K57381,
-    GR/K77051) and by ESPRIT project 6453: Types.}
+    GR/K77051, GR/M75440) and by ESPRIT (projects 3245:
+    Logical Frameworks, and 6453: Types) and by the DFG Schwerpunktprogramm
+    \emph{Deduktion}.}
 }
 
 \newcommand\subcaption[1]{\par {\centering\normalsize\sc#1\par}\bigskip