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