diff -r 9c4d5fd41c9b -r f842a75d9624 doc-src/Logics/logics.bbl
--- a/doc-src/Logics/logics.bbl	Thu Apr 10 14:26:01 1997 +0200
+++ b/doc-src/Logics/logics.bbl	Thu Apr 10 18:07:27 1997 +0200
@@ -126,11 +126,37 @@
 \newblock {\em Intuitionistic type theory}.
 \newblock Bibliopolis, 1984.
 
+\bibitem{milner78}
+Robin Milner.
+\newblock A theory of type polymorphism in programming.
+\newblock {\em Journal of Computer and System Sciences}, 17:348--375, 1978.
+
 \bibitem{milner-coind}
 Robin Milner and Mads Tofte.
 \newblock Co-induction in relational semantics.
 \newblock {\em Theoretical Computer Science}, 87:209--220, 1991.
 
+\bibitem{nazareth-nipkow}
+Dieter Nazareth and Tobias Nipkow.
+\newblock Formal verification of algorithm {W}: The monomorphic case.
+\newblock In J.~von Wright, J.~Grundy, and J.~Harrison, editors, {\em Theorem
+  Proving in Higher Order Logics: {TPHOLs} '96}, LNCS 1125, pages 331--345,
+  1996.
+
+\bibitem{Nipkow-CR}
+Tobias Nipkow.
+\newblock More {Church-Rosser} proofs (in {Isabelle/HOL}).
+\newblock In Michael McRobbie and John~K. Slaney, editors, {\em Automated
+  Deduction --- {CADE}-13 International Conference}, LNAI 1104, pages 733--747.
+  Springer, 1996.
+
+\bibitem{nipkow-IMP}
+Tobias Nipkow.
+\newblock Winskel is (almost) right: Towards a mechanized semantics textbook.
+\newblock In V.~Chandru and V.~Vinay, editors, {\em Foundations of Software
+  Technology and Theoretical Computer Science}, volume 1180 of {\em LNCS},
+  pages 180--192. Springer, 1996.
+
 \bibitem{noel}
 Philippe No{\"e}l.
 \newblock Experimenting with {Isabelle} in {ZF} set theory.
@@ -173,10 +199,23 @@
 \newblock Set theory for verification: {II}. {Induction} and recursion.
 \newblock {\em Journal of Automated Reasoning}, 15(2):167--215, 1995.
 
+\bibitem{paulson-ns}
+Lawrence~C. Paulson.
+\newblock Mechanized proofs of security protocols: {Needham-Schroeder} with
+  public keys.
+\newblock Technical Report 413, Computer Laboratory, University of Cambridge,
+  January 1997.
+
 \bibitem{paulson-coind}
 Lawrence~C. Paulson.
 \newblock Mechanizing coinduction and corecursion in higher-order logic.
-\newblock {\em Journal of Logic and Computation}, 7(2), March 1997.
+\newblock {\em Journal of Logic and Computation}, 7(2):175--204, March 1997.
+
+\bibitem{paulson-security}
+Lawrence~C. Paulson.
+\newblock Proving properties of security protocols by induction.
+\newblock In {\em 10th Computer Security Foundations Workshop}. IEEE Computer
+  Society Press, 1997.
 \newblock In press.
 
 \bibitem{paulson-COLOG}
@@ -197,7 +236,7 @@
 F.~J. Pelletier.
 \newblock Seventy-five problems for testing automatic theorem provers.
 \newblock {\em Journal of Automated Reasoning}, 2:191--216, 1986.
-\newblock Errata, JAR 4 (1988), 235--236.
+\newblock Errata, JAR 4 (1988), 235--236 and JAR 18 (1997), 135.
 
 \bibitem{plaisted90}
 David~A. Plaisted.