equal
deleted
inserted
replaced
16 |
16 |
17 ## Slides |
17 ## Slides |
18 |
18 |
19 session: ./ROOT.ML ./*.thy |
19 session: ./ROOT.ML ./*.thy |
20 @$(USEDIR) -b -D generated -f ROOT.ML HOL Prio |
20 @$(USEDIR) -b -D generated -f ROOT.ML HOL Prio |
21 |
21 |
22 paper: Paper/ROOT.ML \ |
22 paper: Paper/ROOT.ML \ |
23 Paper/*.thy |
23 Paper/*.thy |
24 @$(USEDIR) -D generated -f ROOT.ML Prio Paper |
24 @$(USEDIR) -D generated -f ROOT.ML Prio Paper |
25 rm -f Paper/generated/*.aux # otherwise latex will fall over |
25 rm -f Paper/generated/*.aux # otherwise latex will fall over |
26 cd Paper/generated ; $(ISABELLE_TOOL) latex -o pdf root.tex |
26 cd Paper/generated ; $(ISABELLE_TOOL) latex -o pdf root.tex |