101 |
101 |
102 \subsubsection*{Acknowledgements} |
102 \subsubsection*{Acknowledgements} |
103 Tobias Nipkow contributed most of the section on defining theories. |
103 Tobias Nipkow contributed most of the section on defining theories. |
104 Stefan Berghofer and Sara Kalvala suggested improvements. |
104 Stefan Berghofer and Sara Kalvala suggested improvements. |
105 |
105 |
106 Tobias Nipkow has made immense contributions to Isabelle, including the |
106 Tobias Nipkow has made immense contributions to Isabelle, including the parser |
107 parser generator, type classes, and the simplifier. Carsten Clasohm and |
107 generator, type classes, and the simplifier. Carsten Clasohm and Markus |
108 Markus Wenzel made major contributions; Sonia Mahjoub and Karin Nimmermann |
108 Wenzel made major contributions; Sonia Mahjoub and Karin Nimmermann also |
109 also helped. Isabelle was developed using Dave Matthews's Standard~{\sc |
109 helped. Isabelle was developed using Dave Matthews's Standard~{\sc ml} |
110 ml} compiler, Poly/{\sc ml}. Many people have contributed to Isabelle's |
110 compiler, Poly/{\sc ml}. Many people have contributed to Isabelle's standard |
111 standard object-logics, including Martin Coen, Philippe de Groote, Philippe |
111 object-logics, including Martin Coen, Philippe de Groote, Philippe No\"el. |
112 No\"el. The research has been funded by the EPSRC (grants |
112 The research has been funded by the EPSRC (grants GR/G53279, GR/H40570, |
113 GR/G53279, GR/H40570, GR/K57381, GR/K77051) |
113 GR/K57381, GR/K77051, GR/M75440) and by ESPRIT (projects 3245: Logical |
114 and by ESPRIT (projects 3245: Logical Frameworks, and 6453: Types). |
114 Frameworks, and 6453: Types), and by the DFG Schwerpunktprogramm |
|
115 \emph{Deduktion}. |
115 |
116 |
116 \newpage |
117 \newpage |
117 \pagestyle{plain} \tableofcontents |
118 \pagestyle{plain} \tableofcontents |
118 \newpage |
119 \newpage |
119 |
120 |