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