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

author | paulson |

Wed, 11 Jul 2001 13:56:15 +0200 | |

changeset 11405 | b6e3ac38397d |

parent 11404 | 280436a346ca |

child 11406 | 2b17622e1929 |

tweak

--- a/doc-src/TutorialI/basics.tex Wed Jul 11 13:55:43 2001 +0200 +++ b/doc-src/TutorialI/basics.tex Wed Jul 11 13:56:15 2001 +0200 @@ -2,11 +2,11 @@ \section{Introduction} -This is a tutorial on how to use the theorem prover Isabelle/HOL as a specification and -verification system. Isabelle is a generic system for implementing logical -formalisms, and Isabelle/HOL is the specialization of Isabelle for -HOL, which abbreviates Higher-Order Logic. We introduce HOL step by step -following the equation +This book is a tutorial on how to use the theorem prover Isabelle/HOL as a +specification and verification system. Isabelle is a generic system for +implementing logical formalisms, and Isabelle/HOL is the specialization +of Isabelle for HOL, which abbreviates Higher-Order Logic. We introduce +HOL step by step following the equation \[ \mbox{HOL} = \mbox{Functional Programming} + \mbox{Logic}. \] We do not assume that the reader is familiar with mathematical logic but that (s)he is used to logical and set theoretic notation, such as covered