--- a/src/HOL/Induct/document/root.tex Fri Jan 20 21:56:34 2023 +0100
+++ b/src/HOL/Induct/document/root.tex Fri Jan 20 22:47:55 2023 +0100
@@ -25,4 +25,7 @@
\parindent 0pt\parskip 0.5ex
\input{session}
+\bibliographystyle{abbrv}
+\bibliography{root}
+
\end{document}