1.1 --- a/doc-src/TutorialI/basics.tex	Thu Mar 15 11:06:33 2001 +0100
     1.2 +++ b/doc-src/TutorialI/basics.tex	Thu Mar 15 13:57:10 2001 +0100
     1.3 @@ -9,13 +9,13 @@
     1.4  following the equation
     1.5  \[ \mbox{HOL} = \mbox{Functional Programming} + \mbox{Logic}. \]
     1.6  We do not assume that the reader is familiar with mathematical logic but that
     1.7 -(s)he is used to logical and set theoretic notation.  In contrast, we do assume
     1.8 -that the reader is familiar with the basic concepts of functional programming.
     1.9 -For excellent introductions consult the textbooks by Bird and
    1.10 -Wadler~\cite{Bird-Wadler} or Paulson~\cite{paulson-ml2}.  Although this
    1.11 -tutorial initially concentrates on functional programming, do not be
    1.12 -misled: HOL can express most mathematical concepts, and functional programming
    1.13 -is just one particularly simple and ubiquitous instance.
    1.14 +(s)he is used to logical and set theoretic notation, such as covered
    1.15 +in a good discrete math course~\cite{Rosen-DMA}. In contrast, we do assume
    1.16 +that the reader is familiar with the basic concepts of functional
    1.17 +programming~\cite{Bird-Haskell,Hudak-Haskell,paulson-ml2,Thompson-Haskell}.
    1.18 +Although this tutorial initially concentrates on functional programming, do
    1.19 +not be misled: HOL can express most mathematical concepts, and functional
    1.20 +programming is just one particularly simple and ubiquitous instance.
    1.21  
    1.22  Isabelle~\cite{paulson-isa-book} is implemented in ML~\cite{SML}.  This has
    1.23  influenced some of Isabelle/HOL's concrete syntax but is otherwise irrelevant

     2.1 --- a/doc-src/manual.bib	Thu Mar 15 11:06:33 2001 +0100
     2.2 +++ b/doc-src/manual.bib	Thu Mar 15 13:57:10 2001 +0100
     2.3 @@ -144,6 +144,10 @@
     2.4  @book{Bird-Wadler,author="Richard Bird and Philip Wadler",
     2.5  title="Introduction to Functional Programming",publisher=PH,year=1988}
     2.6  
     2.7 +@book{Bird-Haskell,author="Richard Bird",
     2.8 +title="Introduction to Functional Programming using Haskell",
     2.9 +publisher=PH,year=1998}
    2.10 +
    2.11  @Article{boyer86,
    2.12    author	= {Robert Boyer and Ewing Lusk and William McCune and Ross
    2.13  		   Overbeek and Mark Stickel and Lawrence Wos},
    2.14 @@ -410,6 +414,9 @@
    2.15    number	= 5,
    2.16    month		= May}
    2.17  
    2.18 +@book{Hudak-Haskell,author={Paul Hudak},
    2.19 +title={The Haskell School of Expression},publisher=CUP,year=2000}
    2.20 +
    2.21  @article{huet75,
    2.22    author	= {G. P. Huet},
    2.23    title		= {A Unification Algorithm for Typed $\lambda$-Calculus},
    2.24 @@ -923,6 +930,10 @@
    2.25    publisher	= {Addison-Wesley},
    2.26    year		= 1990}
    2.27  
    2.28 +@book{Rosen-DMA,author={Kenneth H. Rosen},
    2.29 +title={Discrete Mathematics and Its Applications},
    2.30 +publisher={McGraw-Hill},year=1998}
    2.31 +
    2.32  @InProceedings{Rudnicki:1992:MizarOverview,
    2.33    author = 	 {P. Rudnicki},
    2.34    title = 	 {An Overview of the {MIZAR} Project},
    2.35 @@ -1001,6 +1012,10 @@
    2.36    publisher	= {Addison-Wesley},
    2.37    year		= 1991}
    2.38  
    2.39 +@book{Thompson-Haskell,author={Simon Thompson},
    2.40 +title={Haskell: The Craft of Functional Programming},
    2.41 +publisher={Addison-Wesley},year=1999}
    2.42 +
    2.43  @Unpublished{Trybulec:1993:MizarFeatures,
    2.44    author = 	 {A. Trybulec},
    2.45    title = 	 {Some Features of the {Mizar} Language},