1.1 --- a/doc-src/manual.bib	Sun May 21 01:16:54 2000 +0200
     1.2 +++ b/doc-src/manual.bib	Sun May 21 01:17:12 2000 +0200
     1.3 @@ -526,6 +526,23 @@
     1.4    pages		= {317-332},
     1.5    year		= 1998}
     1.6  
     1.7 +@InCollection{nipkow-sorts93,
     1.8 +  author = 	 {T. Nipkow},
     1.9 +  title = 	 {Order-Sorted Polymorphism in {Isabelle}},
    1.10 +  booktitle = 	 {Logical Environments},
    1.11 +  publisher =	 CUP,
    1.12 +  year =	 1993,
    1.13 +  editor =	 {G. Huet and G. Plotkin},
    1.14 +  pages =	 {164--188}
    1.15 +}
    1.16 +
    1.17 +@Misc{nipkow-types93,
    1.18 +  author =	 {Tobias Nipkow},
    1.19 +  title =	 {Axiomatic Type Classes (in {I}sabelle)},
    1.20 +  howpublished = {Presentation at the workshop \emph{Types for Proof and Programs}, Nijmegen},
    1.21 +  year =	 1993
    1.22 +}
    1.23 +
    1.24  @inproceedings{Nipkow-CR,
    1.25    author	= {Tobias Nipkow},
    1.26    title		= {More {Church-Rosser} Proofs (in {Isabelle/HOL})},
    1.27 @@ -558,7 +575,8 @@
    1.28    author	= {Tobias Nipkow and Lawrence C. Paulson and Markus Wenzel},
    1.29    title		= {{Isabelle}'s Logics: {HOL}},
    1.30    institution	= {Institut f\"ur Informatik, Technische Universi\"at
    1.31 -                  M\"unchen and Computer Laboratory, University of Cambridge}}
    1.32 +                  M\"unchen and Computer Laboratory, University of Cambridge},
    1.33 +  note          = {\url{http://isabelle.in.tum.de/doc/logics-HOL.pdf}}}
    1.34  
    1.35  @article{nipkow-prehofer,
    1.36    author	= {Tobias Nipkow and Christian Prehofer},
    1.37 @@ -636,12 +654,14 @@
    1.38  @manual{isabelle-ref,
    1.39    author	= {Lawrence C. Paulson},
    1.40    title		= {The {Isabelle} Reference Manual},
    1.41 -  institution	= CUCL}
    1.42 +  institution	= CUCL,
    1.43 +  note          = {\url{http://isabelle.in.tum.de/doc/ref.pdf}}}
    1.44  
    1.45  @manual{isabelle-ZF,
    1.46    author	= {Lawrence C. Paulson},
    1.47    title		= {{Isabelle}'s Logics: {FOL} and {ZF}},
    1.48 -  institution	= CUCL}
    1.49 +  institution	= CUCL,
    1.50 +  note          = {\url{http://isabelle.in.tum.de/doc/logics-ZF.pdf}}}
    1.51  
    1.52  @article{paulson-found,
    1.53    author	= {Lawrence C. Paulson},
    1.54 @@ -938,12 +958,20 @@
    1.55  @manual{isabelle-sys,
    1.56    author	= {Markus Wenzel and Stefan Berghofer},
    1.57    title		= {The {Isabelle} System Manual},
    1.58 -  institution	= {TU Munich}}
    1.59 +  institution	= {TU Munich},
    1.60 +  note          = {\url{http://isabelle.in.tum.de/doc/system.pdf}}}
    1.61  
    1.62  @manual{isabelle-isar-ref,
    1.63    author	= {Markus Wenzel},
    1.64    title		= {The {Isabelle/Isar} Reference Manual},
    1.65 -  institution	= {TU Munich}}
    1.66 +  institution	= {TU Munich},
    1.67 +  note          = {\url{http://isabelle.in.tum.de/doc/isar-ref.pdf}}}
    1.68 +
    1.69 +@manual{isabelle-axclass,
    1.70 +  author	= {Markus Wenzel},
    1.71 +  title		= {Using Axiomatic Type Classes in {I}sabelle},
    1.72 +  institution	= {TU Munich},
    1.73 +  note          = {\url{http://isabelle.in.tum.de/doc/axclass.pdf}}}
    1.74  
    1.75  
    1.76  @InProceedings{Wenzel:1999:TPHOL,