doc-src/Ref/Makefile
changeset 48939 83bd9eb1c70c
parent 48938 d468d72a458f
child 48940 f0d87c6b7a2e
--- a/doc-src/Ref/Makefile	Mon Aug 27 17:11:55 2012 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,35 +0,0 @@
-
-## targets
-
-default: dvi
-
-
-## dependencies
-
-include ../Makefile.in
-
-NAME = ref
-FILES = ref.tex tactic.tex thm.tex syntax.tex		\
-	substitution.tex simplifier.tex classical.tex ../proof.sty	\
-	../iman.sty ../extra.sty ../ttbox.sty ../manual.bib
-
-dvi: $(NAME).dvi
-
-$(NAME).dvi: $(FILES) isabelle.eps
-	$(LATEX) $(NAME)
-	$(BIBTEX) $(NAME)
-	$(LATEX) $(NAME)
-	$(LATEX) $(NAME)
-	$(SEDINDEX) $(NAME)
-	$(LATEX) $(NAME)
-
-pdf: $(NAME).pdf
-
-$(NAME).pdf: $(FILES) isabelle.pdf
-	$(PDFLATEX) $(NAME)
-	$(BIBTEX) $(NAME)
-	$(PDFLATEX) $(NAME)
-	$(PDFLATEX) $(NAME)
-	$(SEDINDEX) $(NAME)
-	$(FIXBOOKMARKS) $(NAME).out
-	$(PDFLATEX) $(NAME)