# HG changeset patch
# User paulson
# Date 994852575 -7200
# Node ID b6e3ac38397db08341bfcca8bec7816d9df8588c
# Parent  280436a346ca5e416f5bc77065f515722ffa7a18
tweak

diff -r 280436a346ca -r b6e3ac38397d doc-src/TutorialI/basics.tex
--- 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