equal
deleted
inserted
replaced
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 |
|
36 |
|
37 session_itp: Paper/ROOT.ML \ |
|
38 Paper/document/root* \ |
|
39 Paper/*.thy |
|
40 @$(USEDIR) -D generated -f ROOT.ML HOL Paper |
|
41 |
|
42 itp: session_itp |
|
43 rm -f Paper/generated/*.aux # otherwise latex will fall over |
|
44 cd Paper/generated ; $(ISABELLE_TOOL) latex -o pdf root.tex |
|
45 cd Paper/generated ; bibtex root |
|
46 cd Paper/generated ; $(ISABELLE_TOOL) latex -o pdf root.tex |
|
47 cp Paper/generated/root.pdf paper.pdf |
35 |
48 |
36 ## clean |
49 ## clean |
37 |
50 |
38 clean: |
51 clean: |
39 @rm -f $(OUT)/utm |
52 @rm -f $(OUT)/utm |