doc-src/Tutorial/tutorial.bbl
author paulson
Fri, 27 Nov 1998 13:13:22 +0100
changeset 5980 2e9314c07146
parent 5850 9712294e60b9
child 6577 a2b5c84d590a
permissions -rw-r--r--
added Real/Hyperreal
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
5375
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
     1
\begin{thebibliography}{1}
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
     2
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
     3
\bibitem{Bird-Wadler}
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
     4
Richard Bird and Philip Wadler.
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
     5
\newblock {\em Introduction to Functional Programming}.
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
     6
\newblock Prentice-Hall, 1988.
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
     7
5850
9712294e60b9 *** empty log message ***
nipkow
parents: 5375
diff changeset
     8
\bibitem{Gunter-HOL92}
9712294e60b9 *** empty log message ***
nipkow
parents: 5375
diff changeset
     9
Elsa~L. Gunter.
9712294e60b9 *** empty log message ***
nipkow
parents: 5375
diff changeset
    10
\newblock Why we can't have {SML} style datatype declarations in {HOL}.
9712294e60b9 *** empty log message ***
nipkow
parents: 5375
diff changeset
    11
\newblock In L.J.M. Claesen and M.J.C. Gordon, editors, {\em Higher Order Logic
9712294e60b9 *** empty log message ***
nipkow
parents: 5375
diff changeset
    12
  Theorem Proving and its Applications: Proc.\ IFIP TC10/WG10.2 Intl. Workshop,
9712294e60b9 *** empty log message ***
nipkow
parents: 5375
diff changeset
    13
  1992}, pages 561--568. North-Holland, 1993.
9712294e60b9 *** empty log message ***
nipkow
parents: 5375
diff changeset
    14
9712294e60b9 *** empty log message ***
nipkow
parents: 5375
diff changeset
    15
\bibitem{Knuth3-75}
9712294e60b9 *** empty log message ***
nipkow
parents: 5375
diff changeset
    16
Donald~E. Knuth.
9712294e60b9 *** empty log message ***
nipkow
parents: 5375
diff changeset
    17
\newblock {\em The Art of Computer Programming, Volume 3: Sorting and
9712294e60b9 *** empty log message ***
nipkow
parents: 5375
diff changeset
    18
  Searching}.
9712294e60b9 *** empty log message ***
nipkow
parents: 5375
diff changeset
    19
\newblock Addison-Wesley, 1975.
9712294e60b9 *** empty log message ***
nipkow
parents: 5375
diff changeset
    20
9712294e60b9 *** empty log message ***
nipkow
parents: 5375
diff changeset
    21
\bibitem{MuellerNvOS98}
9712294e60b9 *** empty log message ***
nipkow
parents: 5375
diff changeset
    22
Olaf M\"uller, Tobias Nipkow, David~von Oheimb, and Oskar Slotosch.
9712294e60b9 *** empty log message ***
nipkow
parents: 5375
diff changeset
    23
\newblock {HOLCF = HOL + LCF}.
9712294e60b9 *** empty log message ***
nipkow
parents: 5375
diff changeset
    24
\newblock Submitted for publication, 1998.
9712294e60b9 *** empty log message ***
nipkow
parents: 5375
diff changeset
    25
5375
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
    26
\bibitem{Isa-Ref-Man}
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
    27
Lawrence~C. Paulson.
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
    28
\newblock {\em The Isabelle Reference Manual}.
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
    29
\newblock University of Cambridge, Computer Laboratory.
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
    30
\newblock \verb$http://www.in.tum.de/~isabelle/dist/$.
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
    31
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
    32
\bibitem{Isa-Logics-Man}
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
    33
Lawrence~C. Paulson.
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
    34
\newblock {\em Isabelle's Object-Logics}.
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
    35
\newblock University of Cambridge, Computer Laboratory.
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
    36
\newblock \verb$http://www.in.tum.de/~isabelle/dist/$.
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
    37
5850
9712294e60b9 *** empty log message ***
nipkow
parents: 5375
diff changeset
    38
\bibitem{Paulson-LCF}
9712294e60b9 *** empty log message ***
nipkow
parents: 5375
diff changeset
    39
Lawrence~C. Paulson.
9712294e60b9 *** empty log message ***
nipkow
parents: 5375
diff changeset
    40
\newblock {\em Logic and Computation}.
9712294e60b9 *** empty log message ***
nipkow
parents: 5375
diff changeset
    41
\newblock Cambridge University Press, 1987.
9712294e60b9 *** empty log message ***
nipkow
parents: 5375
diff changeset
    42
5375
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
    43
\bibitem{Paulson-ML}
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
    44
Lawrence~C. Paulson.
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
    45
\newblock {\em ML for the Working Programmer}.
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
    46
\newblock Cambridge University Press, 2nd edition, 1996.
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
    47
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
    48
\end{thebibliography}