doc-src/Tutorial/tutorial.bbl

added simple_arity, spec_name, spec_opt_name;
tuned thm_name;
xthms1: no 'and' separators;

\begin{thebibliography}{1}

\bibitem{Bird-Wadler}
Richard Bird and Philip Wadler.
\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}.
\newblock University of Cambridge, Computer Laboratory.
\newblock \verb$http://www.in.tum.de/~isabelle/dist/$.

\bibitem{Isa-Logics-Man}
Lawrence~C. Paulson.
\newblock {\em Isabelle's Object-Logics}.
\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}.
\newblock Cambridge University Press, 2nd edition, 1996.

\end{thebibliography}