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