# HG changeset patch
# User nipkow
# Date 925984106 -7200
# Node ID df9b0abf77e04f4e8f6ee9724e5c0a6a0d009f91
# Parent  94b638b3827c220021315a1cdff38d378e2c5214
More refs.

diff -r 94b638b3827c -r df9b0abf77e0 doc-src/manual.bib
--- a/doc-src/manual.bib	Thu May 06 11:48:09 1999 +0200
+++ b/doc-src/manual.bib	Thu May 06 11:48:26 1999 +0200
@@ -10,6 +10,7 @@
 @string{MIT="MIT Press"}
 @string{NH="North-Holland"}
 @string{Prentice="Prentice-Hall"}
+@string{PH="Prentice-Hall"}
 @string{Springer="Springer-Verlag"}
 
 %institutions
@@ -86,6 +87,9 @@
   crossref	= {huet-plotkin91},
   pages		= {89-119}}
 
+@book{Bird-Wadler,author="Richard Bird and Philip Wadler",
+title="Introduction to Functional Programming",publisher=PH,year=1988}
+
 @Article{boyer86,
   author	= {Robert Boyer and Ewing Lusk and William McCune and Ross
 		   Overbeek and Mark Stickel and Lawrence Wos},
@@ -266,6 +270,13 @@
   publisher	= {Springer},
   series	= {LNCS 78}}
 
+@inproceedings{Gunter-HOL92,author={Elsa L. Gunter},
+title={Why we can't have {SML} style datatype declarations in {HOL}},
+booktitle={Higher Order Logic Theorem Proving and its Applications: Proc.\
+IFIP TC10/WG10.2 Intl. Workshop, 1992},
+editor={L.J.M. Claesen and M.J.C. Gordon},
+publisher=NH,year=1993,pages={561--568}}
+
 @InProceedings{gunter-trees,
   author	= {Elsa L. Gunter},
   title		= {A Broader Class of Trees for Recursive Type Definitions for
@@ -337,6 +348,10 @@
 
 %K
 
+@book{Knuth3-75,author={Donald E. Knuth},
+title={The Art of Computer Programming, Volume 3: Sorting and Searching},
+publisher={Addison-Wesley},year=1975}
+
 @Book{kunen80,
   author	= {Kenneth Kunen},
   title		= {Set Theory: An Introduction to Independence Proofs},
@@ -417,6 +432,11 @@
   school	= {University of Edinburgh},
   year		= 1984}
 
+@article{MuellerNvOS99,
+author=
+{Olaf M\"uller and Tobias Nipkow and Oheimb, David von and Oskar Slotosch},
+title={{HOLCF = HOL + LCF}},journal=JFP,year=1999}
+
 %N
 
 @InProceedings{NaraschewskiW-TPHOLs98,
@@ -475,6 +495,12 @@
   pages		= {171-186},
   year		= 1998}
 
+@manual{isabelle-HOL,
+  author	= {Tobias Nipkow and Lawrence C. Paulson and Markus Wenzel},
+  title		= {{Isabelle}'s Logics: {HOL}},
+  institution	= {Institut f\"ur Informatik, Technische Universi\"at
+                  M\"unchen and Computer Laboratory, University of Cambridge}}
+
 @article{nipkow-prehofer,
   author	= {Tobias Nipkow and Christian Prehofer},
   title		= {Type Reconstruction for Type Classes},
@@ -548,11 +574,13 @@
   month		= mar,
   pages		= {175-204}}
 
-@techreport{isabelle-ZF,
+@manual{isabelle-ref,author="Lawrence C. Paulson",
+title="The Isabelle Reference Manual",organization=CUCL}
+
+@manual{isabelle-ZF,
   author	= {Lawrence C. Paulson},
   title		= {{Isabelle}'s Logics: {FOL} and {ZF}},
-  institution	= CUCL,
-  year		= 1999}
+  institution	= CUCL}
 
 @article{paulson-found,
   author	= {Lawrence C. Paulson},