equal
deleted
inserted
replaced
93 rm -f Slides/generated3/*.aux # otherwise latex will fall over |
93 rm -f Slides/generated3/*.aux # otherwise latex will fall over |
94 cd Slides/generated3 ; $(ISABELLE_TOOL) latex -o pdf root.beamer.tex |
94 cd Slides/generated3 ; $(ISABELLE_TOOL) latex -o pdf root.beamer.tex |
95 cd Slides/generated3 ; $(ISABELLE_TOOL) latex -o pdf root.beamer.tex |
95 cd Slides/generated3 ; $(ISABELLE_TOOL) latex -o pdf root.beamer.tex |
96 cp Slides/generated3/root.beamer.pdf Slides/slides3.pdf |
96 cp Slides/generated3/root.beamer.pdf Slides/slides3.pdf |
97 |
97 |
98 slides: slides1 |
98 session4: Slides/ROOT4.ML \ |
|
99 Slides/document/root* \ |
|
100 Slides/Slides4.thy |
|
101 @$(USEDIR) -D generated4 -f ROOT4.ML HOL-Nominal Slides |
|
102 |
|
103 slides4: session4 |
|
104 rm -f Slides/generated4/*.aux # otherwise latex will fall over |
|
105 cd Slides/generated4 ; $(ISABELLE_TOOL) latex -o pdf root.beamer.tex |
|
106 cd Slides/generated4 ; $(ISABELLE_TOOL) latex -o pdf root.beamer.tex |
|
107 cp Slides/generated4/root.beamer.pdf Slides/slides4.pdf |
|
108 |
|
109 slides: slides4 |
99 |
110 |
100 |
111 |
101 |
112 |
102 |
113 |
103 ## clean |
114 ## clean |