1.1 --- a/doc-src/IsarRef/isar-ref.tex Mon May 08 11:13:11 2000 +0200
1.2 +++ b/doc-src/IsarRef/isar-ref.tex Mon May 08 11:13:28 2000 +0200
1.3 @@ -120,6 +120,6 @@
1.4 \bibliography{../manual}
1.5 \endgroup
1.6
1.7 -\input{isar-ref.ind}
1.8 +\printindex
1.9
1.10 \end{document}