src/HOL/ex/document/root.tex
changeset 12105 1e4451999200
parent 12023 d982f98e0f0d
child 12357 f7fa60115e4e
--- a/src/HOL/ex/document/root.tex	Thu Nov 08 17:54:58 2001 +0100
+++ b/src/HOL/ex/document/root.tex	Thu Nov 08 23:50:08 2001 +0100
@@ -19,4 +19,7 @@
 \parindent 0pt\parskip 0.5ex
 \input{session}
 
+\bibliographystyle{abbrv}
+\bibliography{root}
+
 \end{document}