--- 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},