diff -r 4b9aa15ff713 -r 26b17f2d583e IsaMakefile --- a/IsaMakefile Wed Dec 26 14:52:14 2012 +0000 +++ b/IsaMakefile Wed Dec 26 19:03:06 2012 +0000 @@ -14,7 +14,7 @@ OUT = $(ISABELLE_OUTPUT) LOG = $(OUT)/log -USEDIR = $(ISABELLE_TOOL) usedir -v true -i false -d pdf ## -D generated +USEDIR = $(ISABELLE_TOOL) usedir -v true -i false -D generated ## utm @@ -22,18 +22,14 @@ utm: $(OUT)/utm $(OUT)/utm: *.thy - @$(USEDIR) -b HOL UTM + @$(USEDIR) -f ROOT.ML -b HOL UTM -session: ROOT.ML \ +paper: ROOT.ML \ document/root* \ *.thy - @$(USEDIR) -D generated -f ROOT.ML UTM . - -paper: utm - rm -f generated/*.aux # otherwise latex will fall over - cd generated ; $(ISABELLE_TOOL) latex -o pdf root.tex -# cd generated ; bibtex root -# cd generated ; $(ISABELLE_TOOL) latex -o pdf root.tex + rm -rf generated # otherwise latex will fall over + @$(USEDIR) -f ROOT1.ML UTM . + $(ISABELLE_TOOL) document -o pdf generated cp generated/root.pdf paper.pdf