# HG changeset patch
# User wenzelm
# Date 957777208 -7200
# Node ID 5be2d1745c615260f1f45ac1086ea5ef66aab241
# Parent  5c5c68f4610d5255b7a4d861fe977c4e3736420e
improved indexing;

diff -r 5c5c68f4610d -r 5be2d1745c61 doc-src/HOL/Makefile
--- 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)
diff -r 5c5c68f4610d -r 5be2d1745c61 doc-src/HOL/logics-HOL.tex
--- 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}
diff -r 5c5c68f4610d -r 5be2d1745c61 doc-src/Intro/Makefile
--- 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)
diff -r 5c5c68f4610d -r 5be2d1745c61 doc-src/Intro/intro.tex
--- 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}
diff -r 5c5c68f4610d -r 5be2d1745c61 doc-src/IsarRef/Makefile
--- 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)
diff -r 5c5c68f4610d -r 5be2d1745c61 doc-src/IsarRef/isar-ref.tex
--- 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}
diff -r 5c5c68f4610d -r 5be2d1745c61 doc-src/Logics/Makefile
--- 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)
diff -r 5c5c68f4610d -r 5be2d1745c61 doc-src/Logics/logics.tex
--- 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}
diff -r 5c5c68f4610d -r 5be2d1745c61 doc-src/Ref/Makefile
--- 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)
diff -r 5c5c68f4610d -r 5be2d1745c61 doc-src/Ref/ref.tex
--- 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}
diff -r 5c5c68f4610d -r 5be2d1745c61 doc-src/System/Makefile
--- 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)
diff -r 5c5c68f4610d -r 5be2d1745c61 doc-src/System/system.tex
--- 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}
diff -r 5c5c68f4610d -r 5be2d1745c61 doc-src/Tutorial/Makefile
--- 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)
diff -r 5c5c68f4610d -r 5be2d1745c61 doc-src/Tutorial/tutorial.tex
--- 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}
diff -r 5c5c68f4610d -r 5be2d1745c61 doc-src/TutorialI/Makefile
--- 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)
diff -r 5c5c68f4610d -r 5be2d1745c61 doc-src/TutorialI/tutorial.tex
--- 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}
diff -r 5c5c68f4610d -r 5be2d1745c61 doc-src/ZF/Makefile
--- 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)
diff -r 5c5c68f4610d -r 5be2d1745c61 doc-src/ZF/logics-ZF.tex
--- 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}
diff -r 5c5c68f4610d -r 5be2d1745c61 doc-src/springer.tex
--- 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}