equal
deleted
inserted
replaced
12 |
12 |
13 SRC = $(ISABELLE_HOME)/src |
13 SRC = $(ISABELLE_HOME)/src |
14 OUT = $(ISABELLE_OUTPUT) |
14 OUT = $(ISABELLE_OUTPUT) |
15 LOG = $(OUT)/log |
15 LOG = $(OUT)/log |
16 |
16 |
17 USEDIR = $(ISABELLE_TOOL) usedir -v true -i false -d pdf ## -D generated |
17 USEDIR = $(ISABELLE_TOOL) usedir -v true -i false -D generated |
18 |
18 |
19 |
19 |
20 ## utm |
20 ## utm |
21 |
21 |
22 utm: $(OUT)/utm |
22 utm: $(OUT)/utm |
23 |
23 |
24 $(OUT)/utm: *.thy |
24 $(OUT)/utm: *.thy |
25 @$(USEDIR) -b HOL UTM |
25 @$(USEDIR) -f ROOT.ML -b HOL UTM |
26 |
26 |
27 session: ROOT.ML \ |
27 paper: ROOT.ML \ |
28 document/root* \ |
28 document/root* \ |
29 *.thy |
29 *.thy |
30 @$(USEDIR) -D generated -f ROOT.ML UTM . |
30 rm -rf generated # otherwise latex will fall over |
31 |
31 @$(USEDIR) -f ROOT1.ML UTM . |
32 paper: utm |
32 $(ISABELLE_TOOL) document -o pdf generated |
33 rm -f generated/*.aux # otherwise latex will fall over |
|
34 cd generated ; $(ISABELLE_TOOL) latex -o pdf root.tex |
|
35 # cd generated ; bibtex root |
|
36 # cd generated ; $(ISABELLE_TOOL) latex -o pdf root.tex |
|
37 cp generated/root.pdf paper.pdf |
33 cp generated/root.pdf paper.pdf |
38 |
34 |
39 |
35 |
40 ## clean |
36 ## clean |
41 |
37 |