# 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