diff -r ff8a804e0201 -r 23ceb1dc9755 doc-src/ind-defs.bbl --- a/doc-src/ind-defs.bbl Thu Jan 18 10:28:20 1996 +0100 +++ b/doc-src/ind-defs.bbl Thu Jan 18 10:38:29 1996 +0100 @@ -55,7 +55,7 @@ Huet, G., \newblock Induction principles formalized in the {Calculus of Constructions}, \newblock In {\em Programming of Future Generation Computers\/} (1988), - Elsevier, pp.~205--216 + K.~Fuchi, M.~Nivat, Eds., Elsevier, pp.~205--216 \bibitem{melham89} Melham, T.~F., @@ -98,7 +98,9 @@ \bibitem{paulson-coind} Paulson, L.~C., \newblock Co-induction and co-recursion in higher-order logic, -\newblock Tech. Rep. 304, Comp. Lab., Univ. Cambridge, July 1993 +\newblock Tech. Rep. 304, Comp. Lab., Univ. Cambridge, July 1993, +\newblock To appear in the Festscrift for Alonzo Church, edited by A. Anderson + and M. Zeleny \bibitem{isabelle-intro} Paulson, L.~C., @@ -113,13 +115,14 @@ \bibitem{paulson-set-II} Paulson, L.~C., \newblock Set theory for verification: {II}. {Induction} and recursion, -\newblock Tech. Rep. 312, Comp. Lab., Univ. Cambridge, 1993, -\newblock To appear in J. Auto. Reas. +\newblock {\em J. Auto. Reas. {\bf 15}}, 2 (1995), 167--215 \bibitem{paulson-final} Paulson, L.~C., \newblock A concrete final coalgebra theorem for {ZF} set theory, -\newblock Tech. Rep. 334, Comp. Lab., Univ. Cambridge, 1994 +\newblock In {\em Types for Proofs and Programs: International Workshop {TYPES + '94}\/} (published 1995), P.~Dybjer, B.~Nordstr{\"om},, J.~Smith, Eds., LNCS + 996, Springer, pp.~120--139 \bibitem{pitts94} Pitts, A.~M., @@ -130,8 +133,7 @@ Saaltink, M., Kromodimoeljo, S., Pase, B., Craigen, D., Meisels, I., \newblock An {EVES} data abstraction example, \newblock In {\em FME '93: Industrial-Strength Formal Methods\/} (1993), - J.~C.~P. Woodcock, P.~G. Larsen, Eds., Springer, pp.~578--596, -\newblock LNCS 670 + J.~C.~P. Woodcock, P.~G. Larsen, Eds., LNCS 670, Springer, pp.~578--596 \bibitem{szasz93} Szasz, N.,