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

author | paulson |

Fri, 18 Jan 2002 17:44:15 +0100 | |

changeset 12812 | 6036a579aed4 |

parent 12811 | 894da6aee971 |

child 12813 | f8f0807e5a5e |

tweaks

--- a/doc-src/TutorialI/preface.tex Fri Jan 18 15:17:47 2002 +0100 +++ b/doc-src/TutorialI/preface.tex Fri Jan 18 17:44:15 2002 +0100 @@ -2,7 +2,7 @@ \markboth{Preface}{Preface} This volume is a self-contained introduction to interactive proof -in higher-order logic (HOL), using the proof assistant Isabelle/HOL\@. +in higher-order logic (HOL), using the proof assistant Isabelle 2000. Compared with existing Isabelle documentation, it provides a direct route into higher-order logic, which most people prefer these days. It bypasses first-order logic and minimizes @@ -64,7 +64,7 @@ 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, Norbert Schirmer, Martin Strecker and Markus Wenzel. Stephan +Cornelia Pusch, Norbert Schirmer and Martin Strecker. 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.