equal
deleted
inserted
replaced
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: 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 |
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* \ |
39 Paper/*.thy |
39 Paper/*.thy |
40 @$(USEDIR) -D generated -f ROOT.ML HOL Paper |
40 @$(USEDIR) -D generated -f ROOT.ML UTM Paper |
41 |
41 |
42 itp: session_itp |
42 itp: session_itp |
43 rm -f Paper/generated/*.aux # otherwise latex will fall over |
43 rm -f Paper/generated/*.aux # otherwise latex will fall over |
44 cd Paper/generated ; $(ISABELLE_TOOL) latex -o pdf root.tex |
44 cd Paper/generated ; $(ISABELLE_TOOL) latex -o pdf root.tex |
45 cd Paper/generated ; bibtex root |
45 cd Paper/generated ; bibtex root |