doc-src/TutorialI/basics.tex
changeset 11456 7eb63f63e6c6
parent 11450 1b02a6c4032f
child 12327 5a4d78204492
--- a/doc-src/TutorialI/basics.tex	Wed Jul 25 18:21:01 2001 +0200
+++ b/doc-src/TutorialI/basics.tex	Thu Jul 26 16:43:02 2001 +0200
@@ -8,10 +8,10 @@
 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 you are familiar with mathematical logic but that
-you are used to logical and set theoretic notation, such as covered
-in a good discrete mathematics course~\cite{Rosen-DMA}. 
-In contrast, we do assume
+We do not assume that you are familiar with mathematical logic. 
+However, we do assume that
+you are used to logical and set theoretic notation, as covered
+in a good discrete mathematics course~\cite{Rosen-DMA}, and
 that you are familiar with the basic concepts of functional
 programming~\cite{Bird-Haskell,Hudak-Haskell,paulson-ml2,Thompson-Haskell}.
 Although this tutorial initially concentrates on functional programming, do