# HG changeset patch
# User paulson
# Date 821957909 -3600
# Node ID 23ceb1dc9755a8ad6f0230697d0cc52f54102bf4
# Parent  ff8a804e02010b7be2937946b8cc1560f15a123b
trivial updates

diff -r ff8a804e0201 -r 23ceb1dc9755 doc-src/Logics/logics.bbl
--- a/doc-src/Logics/logics.bbl	Thu Jan 18 10:28:20 1996 +0100
+++ b/doc-src/Logics/logics.bbl	Thu Jan 18 10:38:29 1996 +0100
@@ -112,8 +112,9 @@
 \bibitem{alf}
 Lena Magnusson and Bengt {Nordstr\"om}.
 \newblock The {ALF} proof editor and its proof engine.
-\newblock In {\em Types for Proofs and Programs: International Workshop {TYPES
-  '93}}, LNCS 806, pages 213--237. Springer, published 1994.
+\newblock In Henk Barendregt and Tobias Nipkow, editors, {\em Types for Proofs
+  and Programs: International Workshop {TYPES '93}}, LNCS 806, pages 213--237.
+  Springer, published 1994.
 
 \bibitem{mw81}
 Zohar Manna and Richard Waldinger.
@@ -125,13 +126,6 @@
 \newblock {\em Intuitionistic type theory}.
 \newblock Bibliopolis, 1984.
 
-\bibitem{melham89}
-Thomas~F. Melham.
-\newblock Automating recursive type definitions in higher order logic.
-\newblock In Graham Birtwistle and P.~A. Subrahmanyam, editors, {\em Current
-  Trends in Hardware Verification and Automated Theorem Proving}, pages
-  341--386. Springer, 1989.
-
 \bibitem{milner-coind}
 Robin Milner and Mads Tofte.
 \newblock Co-induction in relational semantics.
@@ -197,8 +191,9 @@
 \bibitem{paulson-final}
 Lawrence~C. Paulson.
 \newblock A concrete final coalgebra theorem for {ZF} set theory.
-\newblock In {\em Types for Proofs and Programs: International Workshop {TYPES
-  '94}}, LNCS 996, pages 120--139. Springer, published 1995.
+\newblock In Peter Dybjer, Bengt Nordstr{\"om}, and Jan Smith, editors, {\em
+  Types for Proofs and Programs: International Workshop {TYPES '94}}, LNCS 996,
+  pages 120--139. Springer, published 1995.
 
 \bibitem{pelletier86}
 F.~J. Pelletier.
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.,