# HG changeset patch
# User lcp
# Date 791002827 -3600
# Node ID 7c82ab7602b4e0c3a3f040085170179f8fd9b16d
# Parent  e528724951b0c5a2acf368f2c4d0133f555a3b47
changed due to new .bib files

diff -r e528724951b0 -r 7c82ab7602b4 doc-src/Logics/logics.bbl
--- a/doc-src/Logics/logics.bbl	Tue Jan 24 12:17:49 1995 +0100
+++ b/doc-src/Logics/logics.bbl	Wed Jan 25 04:00:27 1995 +0100
@@ -165,14 +165,6 @@
 \newblock {\em Logic and Computation: Interactive proof with Cambridge LCF}.
 \newblock Cambridge University Press, 1987.
 
-\bibitem{paulson-COLOG}
-Lawrence~C. Paulson.
-\newblock A formulation of the simple theory of types (for {Isabelle}).
-\newblock In P.~Martin-L\"of and G.~Mints, editors, {\em COLOG-88:
-  International Conference on Computer Logic}, Tallinn, 1990. Estonian Academy
-  of Sciences, Springer.
-\newblock LNCS 417.
-
 \bibitem{paulson-coind}
 Lawrence~C. Paulson.
 \newblock Co-induction and co-recursion in higher-order logic.
@@ -201,8 +193,15 @@
 Lawrence~C. Paulson.
 \newblock A fixedpoint approach to implementing (co)inductive definitions.
 \newblock In Alan Bundy, editor, {\em 12th International Conference on
-  Automated Deduction}, pages 148--161. Springer, 1994.
-\newblock LNAI 814.
+  Automated Deduction}, volume 814, pages 148--161. Springer, 1994.
+
+\bibitem{paulson-COLOG}
+Lawrence~C. Paulson.
+\newblock A formulation of the simple theory of types (for {Isabelle}).
+\newblock In P.~Martin-L\"of and G.~Mints, editors, {\em COLOG-88:
+  International Conference on Computer Logic}, pages 246--274, Tallinn,
+  Published 1990. Estonian Academy of Sciences, Springer.
+\newblock LNCS 417.
 
 \bibitem{pelletier86}
 F.~J. Pelletier.
@@ -228,7 +227,7 @@
 \bibitem{takeuti87}
 G.~Takeuti.
 \newblock {\em Proof Theory}.
-\newblock North Holland, 2nd edition, 1987.
+\newblock North-Holland, 2nd edition, 1987.
 
 \bibitem{thompson91}
 Simon Thompson.
diff -r e528724951b0 -r 7c82ab7602b4 doc-src/Ref/ref.bbl
--- a/doc-src/Ref/ref.bbl	Tue Jan 24 12:17:49 1995 +0100
+++ b/doc-src/Ref/ref.bbl	Wed Jan 25 04:00:27 1995 +0100
@@ -24,9 +24,9 @@
 \bibitem{martin-nipkow}
 Ursula Martin and Tobias Nipkow.
 \newblock Ordered rewriting and confluence.
-\newblock In M.~E. Stickel, editor, {\em 10th International Conference on
+\newblock In Mark~E. Stickel, editor, {\em 10th International Conference on
   Automated Deduction}, pages 366--380. Springer, 1990.
-\newblock LNCS 449.
+\newblock LNAI 449.
 
 \bibitem{Nipkow-LICS-93}
 Tobias Nipkow.