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