improved indexing;
authorwenzelm
Mon May 08 11:13:28 2000 +0200 (2000-05-08)
changeset 88285be2d1745c61
parent 8827 5c5c68f4610d
child 8829 d93e235837a9
improved indexing;
doc-src/HOL/Makefile
doc-src/HOL/logics-HOL.tex
doc-src/Intro/Makefile
doc-src/Intro/intro.tex
doc-src/IsarRef/Makefile
doc-src/IsarRef/isar-ref.tex
doc-src/Logics/Makefile
doc-src/Logics/logics.tex
doc-src/Ref/Makefile
doc-src/Ref/ref.tex
doc-src/System/Makefile
doc-src/System/system.tex
doc-src/Tutorial/Makefile
doc-src/Tutorial/tutorial.tex
doc-src/TutorialI/Makefile
doc-src/TutorialI/tutorial.tex
doc-src/ZF/Makefile
doc-src/ZF/logics-ZF.tex
doc-src/springer.tex
     1.1 --- a/doc-src/HOL/Makefile	Mon May 08 11:13:11 2000 +0200
     1.2 +++ b/doc-src/HOL/Makefile	Mon May 08 11:13:28 2000 +0200
     1.3 @@ -18,7 +18,6 @@
     1.4  dvi: $(NAME).dvi
     1.5  
     1.6  $(NAME).dvi: $(FILES) isabelle_hol.eps
     1.7 -	touch $(NAME).ind
     1.8  	$(LATEX) $(NAME)
     1.9  	$(RAIL) $(NAME)
    1.10  	$(BIBTEX) $(NAME)
    1.11 @@ -30,7 +29,6 @@
    1.12  pdf: $(NAME).pdf
    1.13  
    1.14  $(NAME).pdf: $(FILES) isabelle_hol.pdf
    1.15 -	touch $(NAME).ind
    1.16  	$(PDFLATEX) $(NAME)
    1.17  	$(RAIL) $(NAME)
    1.18  	$(BIBTEX) $(NAME)
     2.1 --- a/doc-src/HOL/logics-HOL.tex	Mon May 08 11:13:11 2000 +0200
     2.2 +++ b/doc-src/HOL/logics-HOL.tex	Mon May 08 11:13:28 2000 +0200
     2.3 @@ -53,5 +53,5 @@
     2.4  \include{HOL}
     2.5  \bibliographystyle{plain}
     2.6  \bibliography{../manual}
     2.7 -\input{logics-HOL.ind}
     2.8 +\printindex
     2.9  \end{document}
     3.1 --- a/doc-src/Intro/Makefile	Mon May 08 11:13:11 2000 +0200
     3.2 +++ b/doc-src/Intro/Makefile	Mon May 08 11:13:28 2000 +0200
     3.3 @@ -18,7 +18,6 @@
     3.4  dvi: $(NAME).dvi
     3.5  
     3.6  $(NAME).dvi: $(FILES) isabelle.eps
     3.7 -	touch $(NAME).ind
     3.8  	$(LATEX) $(NAME)
     3.9  	$(BIBTEX) $(NAME)
    3.10  	$(LATEX) $(NAME)
    3.11 @@ -29,7 +28,6 @@
    3.12  pdf: $(NAME).pdf
    3.13  
    3.14  $(NAME).pdf: $(FILES) isabelle.pdf
    3.15 -	touch $(NAME).ind
    3.16  	$(PDFLATEX) $(NAME)
    3.17  	$(BIBTEX) $(NAME)
    3.18  	$(PDFLATEX) $(NAME)
     4.1 --- a/doc-src/Intro/intro.tex	Mon May 08 11:13:11 2000 +0200
     4.2 +++ b/doc-src/Intro/intro.tex	Mon May 08 11:13:28 2000 +0200
     4.3 @@ -137,5 +137,5 @@
     4.4  \bibliographystyle{plain} \small\raggedright\frenchspacing
     4.5  \bibliography{../manual}
     4.6  
     4.7 -\input{intro.ind}
     4.8 +\printindex
     4.9  \end{document}
     5.1 --- a/doc-src/IsarRef/Makefile	Mon May 08 11:13:11 2000 +0200
     5.2 +++ b/doc-src/IsarRef/Makefile	Mon May 08 11:13:28 2000 +0200
     5.3 @@ -20,7 +20,6 @@
     5.4  dvi: $(NAME).dvi
     5.5  
     5.6  $(NAME).dvi: $(FILES) isabelle_isar.eps
     5.7 -	touch $(NAME).ind
     5.8  	$(LATEX) $(NAME)
     5.9  	$(RAIL) $(NAME)
    5.10  	$(BIBTEX) $(NAME)
    5.11 @@ -32,7 +31,6 @@
    5.12  pdf: $(NAME).pdf
    5.13  
    5.14  $(NAME).pdf: $(FILES) isabelle_isar.pdf
    5.15 -	touch $(NAME).ind
    5.16  	$(PDFLATEX) $(NAME)
    5.17  	$(RAIL) $(NAME)
    5.18  	$(BIBTEX) $(NAME)
     6.1 --- a/doc-src/IsarRef/isar-ref.tex	Mon May 08 11:13:11 2000 +0200
     6.2 +++ b/doc-src/IsarRef/isar-ref.tex	Mon May 08 11:13:28 2000 +0200
     6.3 @@ -120,6 +120,6 @@
     6.4    \bibliography{../manual}
     6.5  \endgroup
     6.6  
     6.7 -\input{isar-ref.ind}
     6.8 +\printindex
     6.9  
    6.10  \end{document}
     7.1 --- a/doc-src/Logics/Makefile	Mon May 08 11:13:11 2000 +0200
     7.2 +++ b/doc-src/Logics/Makefile	Mon May 08 11:13:28 2000 +0200
     7.3 @@ -18,7 +18,6 @@
     7.4  dvi: $(NAME).dvi
     7.5  
     7.6  $(NAME).dvi: $(FILES) isabelle.eps
     7.7 -	touch $(NAME).ind
     7.8  	$(LATEX) $(NAME)
     7.9  	$(BIBTEX) $(NAME)
    7.10  	$(LATEX) $(NAME)
    7.11 @@ -29,7 +28,6 @@
    7.12  pdf: $(NAME).pdf
    7.13  
    7.14  $(NAME).pdf: $(FILES) isabelle.pdf
    7.15 -	touch $(NAME).ind
    7.16  	$(PDFLATEX) $(NAME)
    7.17  	$(BIBTEX) $(NAME)
    7.18  	$(PDFLATEX) $(NAME)
     8.1 --- a/doc-src/Logics/logics.tex	Mon May 08 11:13:11 2000 +0200
     8.2 +++ b/doc-src/Logics/logics.tex	Mon May 08 11:13:28 2000 +0200
     8.3 @@ -47,5 +47,5 @@
     8.4  \include{CTT}
     8.5  \bibliographystyle{plain}
     8.6  \bibliography{../manual}
     8.7 -\input{logics.ind}
     8.8 +\printindex
     8.9  \end{document}
     9.1 --- a/doc-src/Ref/Makefile	Mon May 08 11:13:11 2000 +0200
     9.2 +++ b/doc-src/Ref/Makefile	Mon May 08 11:13:28 2000 +0200
     9.3 @@ -20,7 +20,6 @@
     9.4  dvi: $(NAME).dvi
     9.5  
     9.6  $(NAME).dvi: $(FILES) isabelle.eps
     9.7 -	touch $(NAME).ind
     9.8  	$(LATEX) $(NAME)
     9.9  	$(RAIL) $(NAME)
    9.10  	$(BIBTEX) $(NAME)
    9.11 @@ -32,7 +31,6 @@
    9.12  pdf: $(NAME).pdf
    9.13  
    9.14  $(NAME).pdf: $(FILES) isabelle.pdf
    9.15 -	touch $(NAME).ind
    9.16  	$(PDFLATEX) $(NAME)
    9.17  	$(RAIL) $(NAME)
    9.18  	$(BIBTEX) $(NAME)
    10.1 --- a/doc-src/Ref/ref.tex	Mon May 08 11:13:11 2000 +0200
    10.2 +++ b/doc-src/Ref/ref.tex	Mon May 08 11:13:28 2000 +0200
    10.3 @@ -67,5 +67,5 @@
    10.4  \endgroup
    10.5  \include{theory-syntax}
    10.6  
    10.7 -\input{ref.ind}
    10.8 +\printindex
    10.9  \end{document}
    11.1 --- a/doc-src/System/Makefile	Mon May 08 11:13:11 2000 +0200
    11.2 +++ b/doc-src/System/Makefile	Mon May 08 11:13:28 2000 +0200
    11.3 @@ -18,7 +18,6 @@
    11.4  dvi: $(NAME).dvi
    11.5  
    11.6  $(NAME).dvi: $(FILES) isabelle.eps
    11.7 -	touch $(NAME).ind
    11.8  	$(LATEX) $(NAME)
    11.9  	$(BIBTEX) $(NAME)
   11.10  	$(LATEX) $(NAME)
   11.11 @@ -29,7 +28,6 @@
   11.12  pdf: $(NAME).pdf
   11.13  
   11.14  $(NAME).pdf: $(FILES) isabelle.pdf
   11.15 -	touch $(NAME).ind
   11.16  	$(PDFLATEX) $(NAME)
   11.17  	$(BIBTEX) $(NAME)
   11.18  	$(PDFLATEX) $(NAME)
    12.1 --- a/doc-src/System/system.tex	Mon May 08 11:13:11 2000 +0200
    12.2 +++ b/doc-src/System/system.tex	Mon May 08 11:13:28 2000 +0200
    12.3 @@ -35,6 +35,6 @@
    12.4    \bibliography{../manual}
    12.5  \endgroup
    12.6  
    12.7 -\input{system.ind}
    12.8 +\printindex
    12.9  
   12.10  \end{document}
    13.1 --- a/doc-src/Tutorial/Makefile	Mon May 08 11:13:11 2000 +0200
    13.2 +++ b/doc-src/Tutorial/Makefile	Mon May 08 11:13:28 2000 +0200
    13.3 @@ -18,7 +18,6 @@
    13.4  dvi: $(NAME).dvi
    13.5  
    13.6  $(NAME).dvi: $(FILES) isabelle_hol.eps
    13.7 -	touch $(NAME).ind
    13.8  	$(LATEX) $(NAME)
    13.9  	$(BIBTEX) $(NAME)
   13.10  	$(LATEX) $(NAME)
   13.11 @@ -29,7 +28,6 @@
   13.12  pdf: $(NAME).pdf
   13.13  
   13.14  $(NAME).pdf: $(FILES) isabelle_hol.pdf
   13.15 -	touch $(NAME).ind
   13.16  	$(PDFLATEX) $(NAME)
   13.17  	$(BIBTEX) $(NAME)
   13.18  	$(PDFLATEX) $(NAME)
    14.1 --- a/doc-src/Tutorial/tutorial.tex	Mon May 08 11:13:11 2000 +0200
    14.2 +++ b/doc-src/Tutorial/tutorial.tex	Mon May 08 11:13:28 2000 +0200
    14.3 @@ -60,5 +60,5 @@
    14.4  
    14.5  \bibliographystyle{plain}
    14.6  \bibliography{../manual}
    14.7 -\input{tutorial.ind}
    14.8 +\printindex
    14.9  \end{document}
    15.1 --- a/doc-src/TutorialI/Makefile	Mon May 08 11:13:11 2000 +0200
    15.2 +++ b/doc-src/TutorialI/Makefile	Mon May 08 11:13:28 2000 +0200
    15.3 @@ -19,7 +19,6 @@
    15.4  dvi: $(NAME).dvi
    15.5  
    15.6  $(NAME).dvi: $(FILES) isabelle_hol.eps
    15.7 -	touch $(NAME).ind
    15.8  	$(LATEX) $(NAME)
    15.9  	$(BIBTEX) $(NAME)
   15.10  	$(LATEX) $(NAME)
   15.11 @@ -30,7 +29,6 @@
   15.12  pdf: $(NAME).pdf
   15.13  
   15.14  $(NAME).pdf: $(FILES) isabelle_hol.pdf
   15.15 -	touch $(NAME).ind
   15.16  	$(PDFLATEX) $(NAME)
   15.17  	$(BIBTEX) $(NAME)
   15.18  	$(PDFLATEX) $(NAME)
    16.1 --- a/doc-src/TutorialI/tutorial.tex	Mon May 08 11:13:11 2000 +0200
    16.2 +++ b/doc-src/TutorialI/tutorial.tex	Mon May 08 11:13:28 2000 +0200
    16.3 @@ -74,5 +74,5 @@
    16.4  
    16.5  \bibliographystyle{plain}
    16.6  \bibliography{../manual}
    16.7 -\input{tutorial.ind}
    16.8 +\printindex
    16.9  \end{document}
    17.1 --- a/doc-src/ZF/Makefile	Mon May 08 11:13:11 2000 +0200
    17.2 +++ b/doc-src/ZF/Makefile	Mon May 08 11:13:28 2000 +0200
    17.3 @@ -18,7 +18,6 @@
    17.4  dvi: $(NAME).dvi
    17.5  
    17.6  $(NAME).dvi: $(FILES) isabelle_zf.eps
    17.7 -	touch $(NAME).ind
    17.8  	$(LATEX) $(NAME)
    17.9  	$(RAIL) $(NAME)
   17.10  	$(BIBTEX) $(NAME)
   17.11 @@ -30,7 +29,6 @@
   17.12  pdf: $(NAME).pdf
   17.13  
   17.14  $(NAME).pdf: $(FILES) isabelle_zf.pdf
   17.15 -	touch $(NAME).ind
   17.16  	$(PDFLATEX) $(NAME)
   17.17  	$(RAIL) $(NAME)
   17.18  	$(BIBTEX) $(NAME)
    18.1 --- a/doc-src/ZF/logics-ZF.tex	Mon May 08 11:13:11 2000 +0200
    18.2 +++ b/doc-src/ZF/logics-ZF.tex	Mon May 08 11:13:28 2000 +0200
    18.3 @@ -51,5 +51,5 @@
    18.4  \include{ZF}
    18.5  \bibliographystyle{plain}
    18.6  \bibliography{../manual}
    18.7 -\input{logics-ZF.ind}
    18.8 +\printindex
    18.9  \end{document}
    19.1 --- a/doc-src/springer.tex	Mon May 08 11:13:11 2000 +0200
    19.2 +++ b/doc-src/springer.tex	Mon May 08 11:13:28 2000 +0200
    19.3 @@ -106,5 +106,5 @@
    19.4  \bibliographystyle{springer} \small\raggedright\frenchspacing
    19.5  \bibliography{string-abbrv,atp,funprog,general,isabelle,logicprog,theory}
    19.6  
    19.7 -\input{springer.ind}
    19.8 +\printindex
    19.9  \end{document}