# HG changeset patch
# User wenzelm
# Date 966271377 -7200
# Node ID 48d438b316c99e667d2396e051ac18299b593f24
# Parent  65ee72db023611c4decd8165feefab9fde8a91ea
Aspinall:2000:eProof;
Muzalewski:Mizar;
Wiedijk:1999:Mizar;
Wiedijk:2000:MV;

diff -r 65ee72db0236 -r 48d438b316c9 doc-src/manual.bib
--- a/doc-src/manual.bib	Mon Aug 14 18:14:54 2000 +0200
+++ b/doc-src/manual.bib	Mon Aug 14 18:42:57 2000 +0200
@@ -80,6 +80,14 @@
   series	= "Computer Science and Applied Mathematics",
   year		= 1986}
 
+@InProceedings{Aspinall:2000:eProof,
+  author = 	 {David Aspinall},
+  title = 	 {Protocols for Interactive {e-Proof}},
+  booktitle = 	 {Theorem Proving in Higher Order Logics (TPHOLs)},
+  year =	 2000,
+  note =	 {Unpublished work-in-progress paper,
+                  \url{http://zermelo.dcs.ed.ac.uk/~da/drafts/eproof.ps.gz}}
+}
 @InProceedings{Aspinall:TACAS:2000,
   author = 	 {David Aspinall},
   title = 	 {Proof General: A Generic Tool for Proof Development},
@@ -114,9 +122,10 @@
   title = 	 {Computer-Assisted Mathematics at Work --- The {H}ahn-{B}anach Theorem in
       {I}sabelle/{I}sar},
   booktitle = 	 {Types for Proofs and Programs: TYPES'99},
+  editor =       {Thierry Coquand and Peter Dybjer and Bengt Nordstr{\"o}m
+                  and Jan Smith},
   series =	 {LNCS},
-  year =	 2000,
-  note =	 {To appear}
+  year =	 2000
 }
 
 @InProceedings{Berghofer-Wenzel:1999:TPHOL,
@@ -508,6 +517,15 @@
 {Olaf M\"uller and Tobias Nipkow and Oheimb, David von and Oscar Slotosch},
 title={{HOLCF = HOL + LCF}},journal=JFP,year=1999}
 
+@Manual{Muzalewski:Mizar,
+  title = 	 {An Outline of {PC} {Mizar}},
+  author =	 {Micha{\l} Muzalewski},
+  organization = {Fondation of Logic, Mathematics and Informatics
+                  --- Mizar Users Group},
+  year =	 1993,
+  note =	 {\url{http://www.cs.kun.nl/~freek/mizar/mizarmanual.ps.gz}}
+}
+
 %N
 
 @InProceedings{NaraschewskiW-TPHOLs98,
@@ -1004,6 +1022,22 @@
   note		= {Paperback edition to *56,
   abridged from the 2nd edition (1927)}}
 
+@Misc{Wiedijk:1999:Mizar,
+  author =	 {Freek Wiedijk},
+  title =	 {Mizar: An Impression},
+  howpublished = {Unpublished paper},
+  year =         1999,
+  note =	 {\url{http://www.cs.kun.nl/~freek/mizar/mizarintro.ps.gz}}
+}
+
+@Misc{Wiedijk:2000:MV,
+  author =	 {Freek Wiedijk},
+  title =	 {The Mathematical Vernacular},
+  howpublished = {Unpublished paper},
+  year =         2000,
+  note =	 {\url{http://www.cs.kun.nl/~freek/notes/mv.ps.gz}}
+}
+
 @book{winskel93,
   author	= {Glynn Winskel},
   title		= {The Formal Semantics of Programming Languages},