1.1 --- a/doc-src/manual.bib	Thu May 06 11:48:09 1999 +0200
     1.2 +++ b/doc-src/manual.bib	Thu May 06 11:48:26 1999 +0200
     1.3 @@ -10,6 +10,7 @@
     1.4  @string{MIT="MIT Press"}
     1.5  @string{NH="North-Holland"}
     1.6  @string{Prentice="Prentice-Hall"}
     1.7 +@string{PH="Prentice-Hall"}
     1.8  @string{Springer="Springer-Verlag"}
     1.9  
    1.10  %institutions
    1.11 @@ -86,6 +87,9 @@
    1.12    crossref	= {huet-plotkin91},
    1.13    pages		= {89-119}}
    1.14  
    1.15 +@book{Bird-Wadler,author="Richard Bird and Philip Wadler",
    1.16 +title="Introduction to Functional Programming",publisher=PH,year=1988}
    1.17 +
    1.18  @Article{boyer86,
    1.19    author	= {Robert Boyer and Ewing Lusk and William McCune and Ross
    1.20  		   Overbeek and Mark Stickel and Lawrence Wos},
    1.21 @@ -266,6 +270,13 @@
    1.22    publisher	= {Springer},
    1.23    series	= {LNCS 78}}
    1.24  
    1.25 +@inproceedings{Gunter-HOL92,author={Elsa L. Gunter},
    1.26 +title={Why we can't have {SML} style datatype declarations in {HOL}},
    1.27 +booktitle={Higher Order Logic Theorem Proving and its Applications: Proc.\
    1.28 +IFIP TC10/WG10.2 Intl. Workshop, 1992},
    1.29 +editor={L.J.M. Claesen and M.J.C. Gordon},
    1.30 +publisher=NH,year=1993,pages={561--568}}
    1.31 +
    1.32  @InProceedings{gunter-trees,
    1.33    author	= {Elsa L. Gunter},
    1.34    title		= {A Broader Class of Trees for Recursive Type Definitions for
    1.35 @@ -337,6 +348,10 @@
    1.36  
    1.37  %K
    1.38  
    1.39 +@book{Knuth3-75,author={Donald E. Knuth},
    1.40 +title={The Art of Computer Programming, Volume 3: Sorting and Searching},
    1.41 +publisher={Addison-Wesley},year=1975}
    1.42 +
    1.43  @Book{kunen80,
    1.44    author	= {Kenneth Kunen},
    1.45    title		= {Set Theory: An Introduction to Independence Proofs},
    1.46 @@ -417,6 +432,11 @@
    1.47    school	= {University of Edinburgh},
    1.48    year		= 1984}
    1.49  
    1.50 +@article{MuellerNvOS99,
    1.51 +author=
    1.52 +{Olaf M\"uller and Tobias Nipkow and Oheimb, David von and Oskar Slotosch},
    1.53 +title={{HOLCF = HOL + LCF}},journal=JFP,year=1999}
    1.54 +
    1.55  %N
    1.56  
    1.57  @InProceedings{NaraschewskiW-TPHOLs98,
    1.58 @@ -475,6 +495,12 @@
    1.59    pages		= {171-186},
    1.60    year		= 1998}
    1.61  
    1.62 +@manual{isabelle-HOL,
    1.63 +  author	= {Tobias Nipkow and Lawrence C. Paulson and Markus Wenzel},
    1.64 +  title		= {{Isabelle}'s Logics: {HOL}},
    1.65 +  institution	= {Institut f\"ur Informatik, Technische Universi\"at
    1.66 +                  M\"unchen and Computer Laboratory, University of Cambridge}}
    1.67 +
    1.68  @article{nipkow-prehofer,
    1.69    author	= {Tobias Nipkow and Christian Prehofer},
    1.70    title		= {Type Reconstruction for Type Classes},
    1.71 @@ -548,11 +574,13 @@
    1.72    month		= mar,
    1.73    pages		= {175-204}}
    1.74  
    1.75 -@techreport{isabelle-ZF,
    1.76 +@manual{isabelle-ref,author="Lawrence C. Paulson",
    1.77 +title="The Isabelle Reference Manual",organization=CUCL}
    1.78 +
    1.79 +@manual{isabelle-ZF,
    1.80    author	= {Lawrence C. Paulson},
    1.81    title		= {{Isabelle}'s Logics: {FOL} and {ZF}},
    1.82 -  institution	= CUCL,
    1.83 -  year		= 1999}
    1.84 +  institution	= CUCL}
    1.85  
    1.86  @article{paulson-found,
    1.87    author	= {Lawrence C. Paulson},