doc-src/IsarImplementation/Makefile
author haftmann
Fri Dec 29 12:11:04 2006 +0100 (2006-12-29)
changeset 21927 9677abe5d374
parent 18537 2681f9e34390
child 26905 5cde053f16b8
permissions -rw-r--r--
added handling for explicit classrel witnesses
wenzelm@18537
     1
#
wenzelm@18537
     2
# $Id$
wenzelm@18537
     3
#
wenzelm@18537
     4
wenzelm@18537
     5
## targets
wenzelm@18537
     6
wenzelm@18537
     7
default: dvi
wenzelm@18537
     8
wenzelm@18537
     9
wenzelm@18537
    10
## dependencies
wenzelm@18537
    11
wenzelm@18537
    12
include ../Makefile.in
wenzelm@18537
    13
wenzelm@18537
    14
MAKEGLOSSARY = ./makeglossary
wenzelm@18537
    15
wenzelm@18537
    16
NAME = implementation
wenzelm@18537
    17
wenzelm@18537
    18
FILES = implementation.tex intro.tex Thy/document/prelim.tex Thy/document/logic.tex \
wenzelm@18537
    19
  Thy/document/tactic.tex Thy/document/proof.tex Thy/document/locale.tex \
wenzelm@18537
    20
  Thy/document/integration.tex style.sty ../iman.sty ../extra.sty ../isar.sty \
wenzelm@18537
    21
  ../manual.bib ../proof.sty
wenzelm@18537
    22
wenzelm@18537
    23
dvi: $(NAME).dvi
wenzelm@18537
    24
wenzelm@18537
    25
$(NAME).dvi: $(FILES) isabelle_isar.eps
wenzelm@18537
    26
	$(LATEX) $(NAME)
wenzelm@18537
    27
	$(BIBTEX) $(NAME)
wenzelm@18537
    28
	$(LATEX) $(NAME)
wenzelm@18537
    29
	$(LATEX) $(NAME)
wenzelm@18537
    30
	$(MAKEGLOSSARY) $(NAME)
wenzelm@18537
    31
	$(SEDINDEX) $(NAME)
wenzelm@18537
    32
	$(LATEX) $(NAME)
wenzelm@18537
    33
	$(LATEX) $(NAME)
wenzelm@18537
    34
wenzelm@18537
    35
pdf: $(NAME).pdf
wenzelm@18537
    36
wenzelm@18537
    37
$(NAME).pdf: $(FILES) isabelle_isar.pdf
wenzelm@18537
    38
	$(PDFLATEX) $(NAME)
wenzelm@18537
    39
	$(BIBTEX) $(NAME)
wenzelm@18537
    40
	$(PDFLATEX) $(NAME)
wenzelm@18537
    41
	$(PDFLATEX) $(NAME)
wenzelm@18537
    42
	$(MAKEGLOSSARY) $(NAME)
wenzelm@18537
    43
	$(SEDINDEX) $(NAME)
wenzelm@18537
    44
	$(FIXBOOKMARKS) $(NAME).out
wenzelm@18537
    45
	$(PDFLATEX) $(NAME)
wenzelm@18537
    46
	$(PDFLATEX) $(NAME)