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 generated |
17 USEDIR = $(ISABELLE_TOOL) usedir -v true -i false |
18 |
18 |
19 |
19 |
20 ## utm |
20 ## utm |
21 |
21 |
22 utm: $(OUT)/utm |
22 utm: $(OUT)/utm |
23 |
23 |
24 $(OUT)/utm: thys/*.thy ROOT.ML |
24 $(OUT)/utm: thys/*.thy ROOT.ML |
25 @$(USEDIR) -f ROOT.ML -b HOL UTM |
25 @$(USEDIR) -f ROOT.ML -b HOL UTM |
26 |
26 |
27 paper: ROOT.ML \ |
27 #paper: ROOT.ML \ |
28 document/root* \ |
28 # document/root* \ |
29 *.thy |
29 # *.thy |
30 rm -rf generated # otherwise latex will fall over |
30 # rm -rf generated # otherwise latex will fall over |
31 @$(USEDIR) -f ROOT1.ML UTM . |
31 # @$(USEDIR) -f ROOT1.ML UTM . |
32 $(ISABELLE_TOOL) document -o pdf generated |
32 # $(ISABELLE_TOOL) document -o pdf generated |
33 cp generated/root.pdf paper.pdf |
33 # cp generated/root.pdf paper.pdf |
34 |
34 |
35 ## ITP itp |
35 ## ITP itp |
36 |
36 |
37 session_itp: Paper/ROOT.ML \ |
37 session_itp: Paper/ROOT.ML \ |
38 Paper/document/root* \ |
38 Paper/document/root* \ |