diff -r 59d5fe89f787 -r 9712294e60b9 doc-src/Tutorial/tutorial.bbl --- a/doc-src/Tutorial/tutorial.bbl Thu Nov 12 11:27:36 1998 +0100 +++ b/doc-src/Tutorial/tutorial.bbl Thu Nov 12 16:45:17 1998 +0100 @@ -5,6 +5,24 @@ \newblock {\em Introduction to Functional Programming}. \newblock Prentice-Hall, 1988. +\bibitem{Gunter-HOL92} +Elsa~L. Gunter. +\newblock Why we can't have {SML} style datatype declarations in {HOL}. +\newblock In L.J.M. Claesen and M.J.C. Gordon, editors, {\em Higher Order Logic + Theorem Proving and its Applications: Proc.\ IFIP TC10/WG10.2 Intl. Workshop, + 1992}, pages 561--568. North-Holland, 1993. + +\bibitem{Knuth3-75} +Donald~E. Knuth. +\newblock {\em The Art of Computer Programming, Volume 3: Sorting and + Searching}. +\newblock Addison-Wesley, 1975. + +\bibitem{MuellerNvOS98} +Olaf M\"uller, Tobias Nipkow, David~von Oheimb, and Oskar Slotosch. +\newblock {HOLCF = HOL + LCF}. +\newblock Submitted for publication, 1998. + \bibitem{Isa-Ref-Man} Lawrence~C. Paulson. \newblock {\em The Isabelle Reference Manual}. @@ -17,6 +35,11 @@ \newblock University of Cambridge, Computer Laboratory. \newblock \verb$http://www.in.tum.de/~isabelle/dist/$. +\bibitem{Paulson-LCF} +Lawrence~C. Paulson. +\newblock {\em Logic and Computation}. +\newblock Cambridge University Press, 1987. + \bibitem{Paulson-ML} Lawrence~C. Paulson. \newblock {\em ML for the Working Programmer}.