equal
deleted
inserted
replaced
166 rm -f Slides/generated8/*.aux # otherwise latex will fall over |
166 rm -f Slides/generated8/*.aux # otherwise latex will fall over |
167 cd Slides/generated8 ; $(ISABELLE_TOOL) latex -o pdf root.beamer.tex |
167 cd Slides/generated8 ; $(ISABELLE_TOOL) latex -o pdf root.beamer.tex |
168 cd Slides/generated8 ; $(ISABELLE_TOOL) latex -o pdf root.beamer.tex |
168 cd Slides/generated8 ; $(ISABELLE_TOOL) latex -o pdf root.beamer.tex |
169 cp Slides/generated8/root.beamer.pdf Slides/slides8.pdf |
169 cp Slides/generated8/root.beamer.pdf Slides/slides8.pdf |
170 |
170 |
171 slides: slides1 slides2 slides3 slides4 slides5 slides6 slides7 slides8 |
171 session9: Slides/ROOT9.ML \ |
|
172 Slides/document/root* \ |
|
173 Slides/Slides6.thy |
|
174 @$(USEDIR) -D generated9 -f ROOT9.ML HOL-Nominal Slides |
|
175 |
|
176 slides9: session9 |
|
177 rm -f Slides/generated9/*.aux # otherwise latex will fall over |
|
178 cd Slides/generated9 ; $(ISABELLE_TOOL) latex -o pdf root.beamer.tex |
|
179 cd Slides/generated9 ; $(ISABELLE_TOOL) latex -o pdf root.beamer.tex |
|
180 cp Slides/generated9/root.beamer.pdf Slides/slides9.pdf |
|
181 |
|
182 |
|
183 slides: slides1 slides2 slides3 slides4 slides5 slides6 slides7 slides8 slides8 |
172 |
184 |
173 |
185 |
174 |
186 |
175 |
187 |
176 ## clean |
188 ## clean |