--- 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