doc-src/HOL/logics-HOL.tex
changeset 8828 5be2d1745c61
parent 7835 e9cd3f3be589
child 8979 802acc97fdaf
--- a/doc-src/HOL/logics-HOL.tex	Mon May 08 11:13:11 2000 +0200
+++ b/doc-src/HOL/logics-HOL.tex	Mon May 08 11:13:28 2000 +0200
@@ -53,5 +53,5 @@
 \include{HOL}
 \bibliographystyle{plain}
 \bibliography{../manual}
-\input{logics-HOL.ind}
+\printindex
 \end{document}