--- a/doc-src/HOL/Makefile Mon May 08 11:13:11 2000 +0200
+++ b/doc-src/HOL/Makefile Mon May 08 11:13:28 2000 +0200
@@ -18,7 +18,6 @@
dvi: $(NAME).dvi
$(NAME).dvi: $(FILES) isabelle_hol.eps
- touch $(NAME).ind
$(LATEX) $(NAME)
$(RAIL) $(NAME)
$(BIBTEX) $(NAME)
@@ -30,7 +29,6 @@
pdf: $(NAME).pdf
$(NAME).pdf: $(FILES) isabelle_hol.pdf
- touch $(NAME).ind
$(PDFLATEX) $(NAME)
$(RAIL) $(NAME)
$(BIBTEX) $(NAME)
--- 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}
--- a/doc-src/Intro/Makefile Mon May 08 11:13:11 2000 +0200
+++ b/doc-src/Intro/Makefile Mon May 08 11:13:28 2000 +0200
@@ -18,7 +18,6 @@
dvi: $(NAME).dvi
$(NAME).dvi: $(FILES) isabelle.eps
- touch $(NAME).ind
$(LATEX) $(NAME)
$(BIBTEX) $(NAME)
$(LATEX) $(NAME)
@@ -29,7 +28,6 @@
pdf: $(NAME).pdf
$(NAME).pdf: $(FILES) isabelle.pdf
- touch $(NAME).ind
$(PDFLATEX) $(NAME)
$(BIBTEX) $(NAME)
$(PDFLATEX) $(NAME)
--- a/doc-src/Intro/intro.tex Mon May 08 11:13:11 2000 +0200
+++ b/doc-src/Intro/intro.tex Mon May 08 11:13:28 2000 +0200
@@ -137,5 +137,5 @@
\bibliographystyle{plain} \small\raggedright\frenchspacing
\bibliography{../manual}
-\input{intro.ind}
+\printindex
\end{document}
--- a/doc-src/IsarRef/Makefile Mon May 08 11:13:11 2000 +0200
+++ b/doc-src/IsarRef/Makefile Mon May 08 11:13:28 2000 +0200
@@ -20,7 +20,6 @@
dvi: $(NAME).dvi
$(NAME).dvi: $(FILES) isabelle_isar.eps
- touch $(NAME).ind
$(LATEX) $(NAME)
$(RAIL) $(NAME)
$(BIBTEX) $(NAME)
@@ -32,7 +31,6 @@
pdf: $(NAME).pdf
$(NAME).pdf: $(FILES) isabelle_isar.pdf
- touch $(NAME).ind
$(PDFLATEX) $(NAME)
$(RAIL) $(NAME)
$(BIBTEX) $(NAME)
--- a/doc-src/IsarRef/isar-ref.tex Mon May 08 11:13:11 2000 +0200
+++ b/doc-src/IsarRef/isar-ref.tex Mon May 08 11:13:28 2000 +0200
@@ -120,6 +120,6 @@
\bibliography{../manual}
\endgroup
-\input{isar-ref.ind}
+\printindex
\end{document}
--- a/doc-src/Logics/Makefile Mon May 08 11:13:11 2000 +0200
+++ b/doc-src/Logics/Makefile Mon May 08 11:13:28 2000 +0200
@@ -18,7 +18,6 @@
dvi: $(NAME).dvi
$(NAME).dvi: $(FILES) isabelle.eps
- touch $(NAME).ind
$(LATEX) $(NAME)
$(BIBTEX) $(NAME)
$(LATEX) $(NAME)
@@ -29,7 +28,6 @@
pdf: $(NAME).pdf
$(NAME).pdf: $(FILES) isabelle.pdf
- touch $(NAME).ind
$(PDFLATEX) $(NAME)
$(BIBTEX) $(NAME)
$(PDFLATEX) $(NAME)
--- a/doc-src/Logics/logics.tex Mon May 08 11:13:11 2000 +0200
+++ b/doc-src/Logics/logics.tex Mon May 08 11:13:28 2000 +0200
@@ -47,5 +47,5 @@
\include{CTT}
\bibliographystyle{plain}
\bibliography{../manual}
-\input{logics.ind}
+\printindex
\end{document}
--- a/doc-src/Ref/Makefile Mon May 08 11:13:11 2000 +0200
+++ b/doc-src/Ref/Makefile Mon May 08 11:13:28 2000 +0200
@@ -20,7 +20,6 @@
dvi: $(NAME).dvi
$(NAME).dvi: $(FILES) isabelle.eps
- touch $(NAME).ind
$(LATEX) $(NAME)
$(RAIL) $(NAME)
$(BIBTEX) $(NAME)
@@ -32,7 +31,6 @@
pdf: $(NAME).pdf
$(NAME).pdf: $(FILES) isabelle.pdf
- touch $(NAME).ind
$(PDFLATEX) $(NAME)
$(RAIL) $(NAME)
$(BIBTEX) $(NAME)
--- a/doc-src/Ref/ref.tex Mon May 08 11:13:11 2000 +0200
+++ b/doc-src/Ref/ref.tex Mon May 08 11:13:28 2000 +0200
@@ -67,5 +67,5 @@
\endgroup
\include{theory-syntax}
-\input{ref.ind}
+\printindex
\end{document}
--- a/doc-src/System/Makefile Mon May 08 11:13:11 2000 +0200
+++ b/doc-src/System/Makefile Mon May 08 11:13:28 2000 +0200
@@ -18,7 +18,6 @@
dvi: $(NAME).dvi
$(NAME).dvi: $(FILES) isabelle.eps
- touch $(NAME).ind
$(LATEX) $(NAME)
$(BIBTEX) $(NAME)
$(LATEX) $(NAME)
@@ -29,7 +28,6 @@
pdf: $(NAME).pdf
$(NAME).pdf: $(FILES) isabelle.pdf
- touch $(NAME).ind
$(PDFLATEX) $(NAME)
$(BIBTEX) $(NAME)
$(PDFLATEX) $(NAME)
--- a/doc-src/System/system.tex Mon May 08 11:13:11 2000 +0200
+++ b/doc-src/System/system.tex Mon May 08 11:13:28 2000 +0200
@@ -35,6 +35,6 @@
\bibliography{../manual}
\endgroup
-\input{system.ind}
+\printindex
\end{document}
--- a/doc-src/Tutorial/Makefile Mon May 08 11:13:11 2000 +0200
+++ b/doc-src/Tutorial/Makefile Mon May 08 11:13:28 2000 +0200
@@ -18,7 +18,6 @@
dvi: $(NAME).dvi
$(NAME).dvi: $(FILES) isabelle_hol.eps
- touch $(NAME).ind
$(LATEX) $(NAME)
$(BIBTEX) $(NAME)
$(LATEX) $(NAME)
@@ -29,7 +28,6 @@
pdf: $(NAME).pdf
$(NAME).pdf: $(FILES) isabelle_hol.pdf
- touch $(NAME).ind
$(PDFLATEX) $(NAME)
$(BIBTEX) $(NAME)
$(PDFLATEX) $(NAME)
--- a/doc-src/Tutorial/tutorial.tex Mon May 08 11:13:11 2000 +0200
+++ b/doc-src/Tutorial/tutorial.tex Mon May 08 11:13:28 2000 +0200
@@ -60,5 +60,5 @@
\bibliographystyle{plain}
\bibliography{../manual}
-\input{tutorial.ind}
+\printindex
\end{document}
--- a/doc-src/TutorialI/Makefile Mon May 08 11:13:11 2000 +0200
+++ b/doc-src/TutorialI/Makefile Mon May 08 11:13:28 2000 +0200
@@ -19,7 +19,6 @@
dvi: $(NAME).dvi
$(NAME).dvi: $(FILES) isabelle_hol.eps
- touch $(NAME).ind
$(LATEX) $(NAME)
$(BIBTEX) $(NAME)
$(LATEX) $(NAME)
@@ -30,7 +29,6 @@
pdf: $(NAME).pdf
$(NAME).pdf: $(FILES) isabelle_hol.pdf
- touch $(NAME).ind
$(PDFLATEX) $(NAME)
$(BIBTEX) $(NAME)
$(PDFLATEX) $(NAME)
--- a/doc-src/TutorialI/tutorial.tex Mon May 08 11:13:11 2000 +0200
+++ b/doc-src/TutorialI/tutorial.tex Mon May 08 11:13:28 2000 +0200
@@ -74,5 +74,5 @@
\bibliographystyle{plain}
\bibliography{../manual}
-\input{tutorial.ind}
+\printindex
\end{document}
--- a/doc-src/ZF/Makefile Mon May 08 11:13:11 2000 +0200
+++ b/doc-src/ZF/Makefile Mon May 08 11:13:28 2000 +0200
@@ -18,7 +18,6 @@
dvi: $(NAME).dvi
$(NAME).dvi: $(FILES) isabelle_zf.eps
- touch $(NAME).ind
$(LATEX) $(NAME)
$(RAIL) $(NAME)
$(BIBTEX) $(NAME)
@@ -30,7 +29,6 @@
pdf: $(NAME).pdf
$(NAME).pdf: $(FILES) isabelle_zf.pdf
- touch $(NAME).ind
$(PDFLATEX) $(NAME)
$(RAIL) $(NAME)
$(BIBTEX) $(NAME)
--- a/doc-src/ZF/logics-ZF.tex Mon May 08 11:13:11 2000 +0200
+++ b/doc-src/ZF/logics-ZF.tex Mon May 08 11:13:28 2000 +0200
@@ -51,5 +51,5 @@
\include{ZF}
\bibliographystyle{plain}
\bibliography{../manual}
-\input{logics-ZF.ind}
+\printindex
\end{document}
--- a/doc-src/springer.tex Mon May 08 11:13:11 2000 +0200
+++ b/doc-src/springer.tex Mon May 08 11:13:28 2000 +0200
@@ -106,5 +106,5 @@
\bibliographystyle{springer} \small\raggedright\frenchspacing
\bibliography{string-abbrv,atp,funprog,general,isabelle,logicprog,theory}
-\input{springer.ind}
+\printindex
\end{document}