doc-src/Tutorial/tutorial.bbl
changeset 5850 9712294e60b9
parent 5375 1463e182c533
child 6577 a2b5c84d590a
--- 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}.