diff -r edd8cb346109 -r 18fea4aa9625 doc-src/Inductive/ind-defs.bbl
--- a/doc-src/Inductive/ind-defs.bbl	Sat Nov 01 12:57:01 1997 +0100
+++ b/doc-src/Inductive/ind-defs.bbl	Sat Nov 01 12:58:08 1997 +0100
@@ -125,13 +125,6 @@
 \newblock In {\em Typed Lambda Calculi and Applications\/} (1993), M.~Bezem
   J.~Groote, Eds., LNCS 664, Springer, pp.~328--345
 
-\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},
@@ -163,6 +156,14 @@
 \newblock A concrete final coalgebra theorem for {ZF} set theory,
 \newblock In Dybjer et~al. \cite{types94}, pp.~120--139
 
+\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, Published
+  1997,
+\newblock In press
+
 \bibitem{paulson-gr}
 Paulson, L.~C., Gr\c{a}bczewski, K.,
 \newblock Mechanizing set theory: Cardinal arithmetic and the axiom of choice,