equal
deleted
inserted
replaced
38 rm -f tphols-2011/generated/*.aux # otherwise latex will fall over |
38 rm -f tphols-2011/generated/*.aux # otherwise latex will fall over |
39 cd tphols-2011/generated ; $(ISABELLE_TOOL) latex -o pdf root.tex |
39 cd tphols-2011/generated ; $(ISABELLE_TOOL) latex -o pdf root.tex |
40 cd tphols-2011/generated ; $(ISABELLE_TOOL) latex -o pdf root.tex |
40 cd tphols-2011/generated ; $(ISABELLE_TOOL) latex -o pdf root.tex |
41 cp tphols-2011/generated/root.pdf tphols-2011/myhill.pdf |
41 cp tphols-2011/generated/root.pdf tphols-2011/myhill.pdf |
42 |
42 |
|
43 ## full paper |
|
44 |
|
45 fullsession2: tphols-2011/ROOT.ML \ |
|
46 tphols-2011/document/root* \ |
|
47 *.thy |
|
48 @$(USEDIR) -D generated -f ROOT.ML HOL tphols-2011 |
|
49 |
|
50 fullpaper: fullsession2 |
|
51 rm -f tphols-2011/generated/*.aux # otherwise latex will fall over |
|
52 cd tphols-2011/generated ; $(ISABELLE_TOOL) latex -o pdf root.tex |
|
53 cd tphols-2011/generated ; $(ISABELLE_TOOL) latex -o pdf root.tex |
|
54 cp tphols-2011/generated/root.pdf tphols-2011/myhill.pdf |
|
55 |
|
56 |
43 |
57 |
44 ## ITP paper |
58 ## ITP paper |
45 |
59 |
46 session3: Paper/ROOT.ML \ |
60 session3: Paper/ROOT.ML \ |
47 Paper/document/root* \ |
61 Paper/document/root* \ |