equal
deleted
inserted
replaced
17 ## Slides |
17 ## Slides |
18 |
18 |
19 session1: Slides/ROOT.ML \ |
19 session1: Slides/ROOT.ML \ |
20 Slides/document/root* \ |
20 Slides/document/root* \ |
21 Slides/Slides.thy |
21 Slides/Slides.thy |
22 @$(USEDIR) -D generated -f ROOT.ML ListP tphols-2011 |
22 @$(USEDIR) -D generated -f ROOT.ML HOL Slides |
23 |
23 |
24 slides: session1 |
24 slides: session1 |
25 rm -f Slides/generated/*.aux # otherwise latex will fall over |
25 rm -f Slides/generated/*.aux # otherwise latex will fall over |
26 cd Slides/generated ; $(ISABELLE_TOOL) latex -o pdf root.beamer.tex |
26 cd Slides/generated ; $(ISABELLE_TOOL) latex -o pdf root.beamer.tex |
27 cp Slides/generated/root.beamer.pdf Slides/slides.pdf |
27 cp Slides/generated/root.beamer.pdf Slides/slides.pdf |
|
28 |
|
29 ## Slides |
|
30 |
|
31 session11: Slides/ROOT.ML \ |
|
32 Slides/document/root* \ |
|
33 Slides/Slides1.thy |
|
34 @$(USEDIR) -D generated -f ROOT1.ML HOL Slides |
|
35 |
|
36 slides1: session11 |
|
37 rm -f Slides/generated/*.aux # otherwise latex will fall over |
|
38 cd Slides/generated ; $(ISABELLE_TOOL) latex -o pdf root.beamer.tex |
|
39 cp Slides/generated/root.beamer.pdf Slides/slides1.pdf |
28 |
40 |
29 |
41 |
30 ## long paper |
42 ## long paper |
31 |
43 |
32 session2: tphols-2011/ROOT.ML \ |
44 session2: tphols-2011/ROOT.ML \ |