diff -r e07927b980ec -r 7eb63f63e6c6 doc-src/TutorialI/basics.tex --- 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