doc-src/Logics/logics.bbl

 \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.
+\newblock In von Wright et~al. \cite{tphols96}, pages 331--345.
 
 \bibitem{Nipkow-CR}
 Tobias Nipkow.
 \newblock More {Church-Rosser} proofs (in {Isabelle/HOL}).
 \newblock In Michael McRobbie and John~K. Slaney, editors, {\em Automated

 \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.
+\newblock In {\em 10th Computer Security Foundations Workshop}, pages 70--83.
+  IEEE Computer Society Press, 1997.
 
 \bibitem{paulson-COLOG}
 Lawrence~C. Paulson.
 \newblock A formulation of the simple theory of types (for {Isabelle}).
 \newblock In P.~Martin-L\"of and G.~Mints, editors, {\em COLOG-88:

 \bibitem{quaife92}
 Art Quaife.
 \newblock Automated deduction in {von Neumann-Bernays-G\"{o}del} set theory.
 \newblock {\em Journal of Automated Reasoning}, 8(1):91--147, 1992.
 
+\bibitem{slind-tfl}
+Konrad Slind.
+\newblock Function definition in higher-order logic.
+\newblock In von Wright et~al. \cite{tphols96}.
+
 \bibitem{suppes72}
 Patrick Suppes.
 \newblock {\em Axiomatic Set Theory}.
 \newblock Dover, 1972.
 

 
 \bibitem{thompson91}
 Simon Thompson.
 \newblock {\em Type Theory and Functional Programming}.
 \newblock Addison-Wesley, 1991.
+
+\bibitem{tphols96}
+J.~von Wright, J.~Grundy, and J.~Harrison, editors.
+\newblock {\em Theorem Proving in Higher Order Logics: {TPHOLs} '96}, LNCS
+  1125, 1996.
 
 \bibitem{principia}
 A.~N. Whitehead and B.~Russell.
 \newblock {\em Principia Mathematica}.
 \newblock Cambridge University Press, 1962.