trivial updates Isabelle94-5
authorpaulson
Thu Jan 18 10:38:29 1996 +0100 (1996-01-18)
changeset 144423ceb1dc9755
parent 1443 ff8a804e0201
child 1445 887e9816eea4
trivial updates
doc-src/Logics/logics.bbl
doc-src/ind-defs.bbl
     1.1 --- a/doc-src/Logics/logics.bbl	Thu Jan 18 10:28:20 1996 +0100
     1.2 +++ b/doc-src/Logics/logics.bbl	Thu Jan 18 10:38:29 1996 +0100
     1.3 @@ -112,8 +112,9 @@
     1.4  \bibitem{alf}
     1.5  Lena Magnusson and Bengt {Nordstr\"om}.
     1.6  \newblock The {ALF} proof editor and its proof engine.
     1.7 -\newblock In {\em Types for Proofs and Programs: International Workshop {TYPES
     1.8 -  '93}}, LNCS 806, pages 213--237. Springer, published 1994.
     1.9 +\newblock In Henk Barendregt and Tobias Nipkow, editors, {\em Types for Proofs
    1.10 +  and Programs: International Workshop {TYPES '93}}, LNCS 806, pages 213--237.
    1.11 +  Springer, published 1994.
    1.12  
    1.13  \bibitem{mw81}
    1.14  Zohar Manna and Richard Waldinger.
    1.15 @@ -125,13 +126,6 @@
    1.16  \newblock {\em Intuitionistic type theory}.
    1.17  \newblock Bibliopolis, 1984.
    1.18  
    1.19 -\bibitem{melham89}
    1.20 -Thomas~F. Melham.
    1.21 -\newblock Automating recursive type definitions in higher order logic.
    1.22 -\newblock In Graham Birtwistle and P.~A. Subrahmanyam, editors, {\em Current
    1.23 -  Trends in Hardware Verification and Automated Theorem Proving}, pages
    1.24 -  341--386. Springer, 1989.
    1.25 -
    1.26  \bibitem{milner-coind}
    1.27  Robin Milner and Mads Tofte.
    1.28  \newblock Co-induction in relational semantics.
    1.29 @@ -197,8 +191,9 @@
    1.30  \bibitem{paulson-final}
    1.31  Lawrence~C. Paulson.
    1.32  \newblock A concrete final coalgebra theorem for {ZF} set theory.
    1.33 -\newblock In {\em Types for Proofs and Programs: International Workshop {TYPES
    1.34 -  '94}}, LNCS 996, pages 120--139. Springer, published 1995.
    1.35 +\newblock In Peter Dybjer, Bengt Nordstr{\"om}, and Jan Smith, editors, {\em
    1.36 +  Types for Proofs and Programs: International Workshop {TYPES '94}}, LNCS 996,
    1.37 +  pages 120--139. Springer, published 1995.
    1.38  
    1.39  \bibitem{pelletier86}
    1.40  F.~J. Pelletier.
     2.1 --- a/doc-src/ind-defs.bbl	Thu Jan 18 10:28:20 1996 +0100
     2.2 +++ b/doc-src/ind-defs.bbl	Thu Jan 18 10:38:29 1996 +0100
     2.3 @@ -55,7 +55,7 @@
     2.4  Huet, G.,
     2.5  \newblock Induction principles formalized in the {Calculus of Constructions},
     2.6  \newblock In {\em Programming of Future Generation Computers\/} (1988),
     2.7 -  Elsevier, pp.~205--216
     2.8 +  K.~Fuchi, M.~Nivat, Eds., Elsevier, pp.~205--216
     2.9  
    2.10  \bibitem{melham89}
    2.11  Melham, T.~F.,
    2.12 @@ -98,7 +98,9 @@
    2.13  \bibitem{paulson-coind}
    2.14  Paulson, L.~C.,
    2.15  \newblock Co-induction and co-recursion in higher-order logic,
    2.16 -\newblock Tech. Rep. 304, Comp. Lab., Univ. Cambridge, July 1993
    2.17 +\newblock Tech. Rep. 304, Comp. Lab., Univ. Cambridge, July 1993,
    2.18 +\newblock To appear in the Festscrift for Alonzo Church, edited by A. Anderson
    2.19 +  and M. Zeleny
    2.20  
    2.21  \bibitem{isabelle-intro}
    2.22  Paulson, L.~C.,
    2.23 @@ -113,13 +115,14 @@
    2.24  \bibitem{paulson-set-II}
    2.25  Paulson, L.~C.,
    2.26  \newblock Set theory for verification: {II}. {Induction} and recursion,
    2.27 -\newblock Tech. Rep. 312, Comp. Lab., Univ. Cambridge, 1993,
    2.28 -\newblock To appear in J. Auto. Reas.
    2.29 +\newblock {\em J. Auto. Reas. {\bf 15}}, 2 (1995), 167--215
    2.30  
    2.31  \bibitem{paulson-final}
    2.32  Paulson, L.~C.,
    2.33  \newblock A concrete final coalgebra theorem for {ZF} set theory,
    2.34 -\newblock Tech. Rep. 334, Comp. Lab., Univ. Cambridge, 1994
    2.35 +\newblock In {\em Types for Proofs and Programs: International Workshop {TYPES
    2.36 +  '94}\/} (published 1995), P.~Dybjer, B.~Nordstr{\"om},, J.~Smith, Eds., LNCS
    2.37 +  996, Springer, pp.~120--139
    2.38  
    2.39  \bibitem{pitts94}
    2.40  Pitts, A.~M.,
    2.41 @@ -130,8 +133,7 @@
    2.42  Saaltink, M., Kromodimoeljo, S., Pase, B., Craigen, D., Meisels, I.,
    2.43  \newblock An {EVES} data abstraction example,
    2.44  \newblock In {\em FME '93: Industrial-Strength Formal Methods\/} (1993),
    2.45 -  J.~C.~P. Woodcock, P.~G. Larsen, Eds., Springer, pp.~578--596,
    2.46 -\newblock LNCS 670
    2.47 +  J.~C.~P. Woodcock, P.~G. Larsen, Eds., LNCS 670, Springer, pp.~578--596
    2.48  
    2.49  \bibitem{szasz93}
    2.50  Szasz, N.,