# HG changeset patch # User paulson # Date 846670509 -3600 # Node ID 217ae06dc291bbacfbde039e2c4b4a3867c158ca # Parent 80477862ab3318cb64ef4eede36dc287031c8e9e Updated references diff -r 80477862ab33 -r 217ae06dc291 doc-src/ind-defs.bbl --- a/doc-src/ind-defs.bbl Mon Oct 28 15:59:39 1996 +0100 +++ b/doc-src/ind-defs.bbl Wed Oct 30 11:15:09 1996 +0100 @@ -109,9 +109,8 @@ \bibitem{nipkow-CR} Nipkow, T., \newblock More {Church-Rosser} proofs (in {Isabelle/HOL}), -\newblock In {\em Automated Deduction --- {CADE}-13\/} (1996), M.~McRobbie - J.~Slaney, Eds., LNAI, Springer, p.~?, -\newblock in press +\newblock In {\em Automated Deduction --- {CADE}-13 International Conference\/} + (1996), M.~McRobbie J.~K. Slaney, Eds., LNAI 1104, Springer, pp.~733--747 \bibitem{pvs-language} Owre, S., Shankar, N., Rushby, J.~M., @@ -126,21 +125,29 @@ \newblock Research Report 92-49, LIP, Ecole Normale Sup\'erieure de Lyon, Dec. 1992 +\bibitem{paulson-markt} +Paulson, L.~C., +\newblock Tool support for logics of programs, +\newblock In {\em Mathematical Methods in Program Development: Summer School + Marktoberdorf 1996}, M.~Broy, Ed., NATO ASI Series F. Springer, +\newblock In press + \bibitem{paulson87} Paulson, L.~C., \newblock {\em Logic and Computation: Interactive proof with Cambridge LCF}, \newblock Cambridge Univ. Press, 1987 -\bibitem{isabelle-intro} -Paulson, L.~C., -\newblock Introduction to {Isabelle}, -\newblock Tech. Rep. 280, Comp. Lab., Univ. Cambridge, 1993 - \bibitem{paulson-set-I} Paulson, L.~C., \newblock Set theory for verification: {I}. {From} foundations to functions, \newblock {\em J. Auto. Reas. {\bf 11}}, 3 (1993), 353--389 +\bibitem{paulson-isa-book} +Paulson, L.~C., +\newblock {\em Isabelle: A Generic Theorem Prover}, +\newblock Springer, 1994, +\newblock LNCS 828 + \bibitem{paulson-set-II} Paulson, L.~C., \newblock Set theory for verification: {II}. {Induction} and recursion, @@ -149,7 +156,7 @@ \bibitem{paulson-coind} Paulson, L.~C., \newblock Mechanizing coinduction and corecursion in higher-order logic, -\newblock {\em J. Logic and Comput.\/} (1996), +\newblock {\em J. Logic and Comput. {\bf 7}}, 2 (Mar. 1997), \newblock In press \bibitem{paulson-final} @@ -185,8 +192,7 @@ Slind, K., \newblock Function definition in higher-order logic, \newblock In {\em Theorem Proving in Higher Order Logics\/} (1996), J.~von - Wright, Ed., -\newblock In press + Wright, J.~Grundy, J.~Harrison, Eds., LNCS 1125 \bibitem{szasz93} Szasz, N.,