doc-src/TutorialI/basics.tex
changeset 11209 a8cb33f6cf9c
parent 11205 67cec35dbc58
child 11213 aeb5c72dd72a
--- a/doc-src/TutorialI/basics.tex	Thu Mar 15 11:06:33 2001 +0100
+++ b/doc-src/TutorialI/basics.tex	Thu Mar 15 13:57:10 2001 +0100
@@ -9,13 +9,13 @@
 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.  In contrast, we do assume
-that the reader is familiar with the basic concepts of functional programming.
-For excellent introductions consult the textbooks by Bird and
-Wadler~\cite{Bird-Wadler} or Paulson~\cite{paulson-ml2}.  Although this
-tutorial initially concentrates on functional programming, do not be
-misled: HOL can express most mathematical concepts, and functional programming
-is just one particularly simple and ubiquitous instance.
+(s)he is used to logical and set theoretic notation, such as covered
+in a good discrete math course~\cite{Rosen-DMA}. In contrast, we do assume
+that the reader is 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
+not be misled: HOL can express most mathematical concepts, and functional
+programming is just one particularly simple and ubiquitous instance.
 
 Isabelle~\cite{paulson-isa-book} is implemented in ML~\cite{SML}.  This has
 influenced some of Isabelle/HOL's concrete syntax but is otherwise irrelevant