summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
raw | gz |
help

author | paulson |

Wed, 11 Jul 2001 15:10:07 +0200 | |

changeset 11408 | 582433f7f618 |

parent 11407 | 138919f1a135 |

child 11409 | f0bcb3dfa7d6 |

new preface

--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/doc-src/TutorialI/preface.tex Wed Jul 11 15:10:07 2001 +0200 @@ -0,0 +1,33 @@ +\chapter*{Preface} +\markboth{Preface}{Preface} + +This volume is a self-contained introduction to interactive proof using +Isabelle/HOL\@. Compared with existing Isabelle documentation, it +provides a straightforward route into higher-order logic, which most +people prefer these days. It bypasses first-order logic and minimizes +discussion of meta-theory. It is written for potential users rather +than for our colleagues in the research world. + +Another departure from previous documentation is the use of Markus +Wenzel's proof script notation instead of ML tactic files. The latter +make it easier to introduce new tactics on the fly, but hardly anybody +does that. Wenzel's dedicated syntax is elegant, replacing for example +eight simplification tactics with a single method, namely \isa{simp}, +with associated options. + +The typesetting relies on Wenzel's proof presentation tools. A possibly +annotated theory file is run, typesetting the theory and any requested +Isabelle responses in the form of a \TeX{} source file. This book is +derived almost entirely from output generated in this way. + +This tutorial owes a lot to the constant discussions with and the valuable +feedback from the Isabelle group at Munich: Stefan Berghofer, Olaf M{\"u}ller, +Wolfgang Naraschewski, David von Oheimb, Leonor Prensa Nieto, Cornelia Pusch, +Martin Strecker and Markus Wenzel. Stephan Merz was also kind enough to +read and comment on a draft version. We received comments from Stefano +Bistarelli, Gergely Buday and Tanja Vos.\REMARK{incomplete list!} + +The research has been funded by many sources, including the {\sc epsrc} +grants GR\slash K57381, GR\slash K77051, +GR\slash M75440, GR\slash R01156\slash 01 and by the \textsc{esprit} +working groups 21900 and IST-1999-29001 (the \emph{Types} project).