used a better implementation of \index in Latex; added more to the theorem section
## targets
default: tutorial
all: tutorial
## global settings
SRC = $(ISABELLE_HOME)/src
OUT = $(ISABELLE_OUTPUT)
LOG = $(OUT)/log
USEDIR = $(ISATOOL) usedir -v true -D generated
tutorial: ProgTutorial/ROOT.ML \
ProgTutorial/document/root.tex \
ProgTutorial/document/root.bib \
ProgTutorial/*.thy \
ProgTutorial/*.ML \
ProgTutorial/Recipes/*.thy \
ProgTutorial/Package/*.thy \
ProgTutorial/Package/*.ML
@rm -rf ProgTutorial/generated/*
$(USEDIR) HOL ProgTutorial
hg parent --template '{date|shortdate}' > ProgTutorial/generated/tip
$(ISATOOL) version > ProgTutorial/generated/version
$(ML_HOME)/poly -v > ProgTutorial/generated/pversion
$(ISATOOL) document -o pdf ProgTutorial/generated
@cp ProgTutorial/document.pdf progtutorial.pdf
## clean
clean:
@rm -f ProgTutorial/generated/*