equal
deleted
inserted
replaced
193 rm -f Slides/generated9/*.aux # otherwise latex will fall over |
193 rm -f Slides/generated9/*.aux # otherwise latex will fall over |
194 cd Slides/generated9 ; $(ISABELLE_TOOL) latex -o pdf root.beamer.tex |
194 cd Slides/generated9 ; $(ISABELLE_TOOL) latex -o pdf root.beamer.tex |
195 cd Slides/generated9 ; $(ISABELLE_TOOL) latex -o pdf root.beamer.tex |
195 cd Slides/generated9 ; $(ISABELLE_TOOL) latex -o pdf root.beamer.tex |
196 cp Slides/generated9/root.beamer.pdf Slides/slides9.pdf |
196 cp Slides/generated9/root.beamer.pdf Slides/slides9.pdf |
197 |
197 |
198 |
198 sessionA: Slides/ROOTA.ML \ |
199 slides: slides1 slides2 slides3 slides4 slides5 slides6 slides7 slides8 slides8 slides9 |
199 Slides/document/root* \ |
|
200 Slides/SlidesA.thy |
|
201 @$(USEDIR) -D generatedA -f ROOTA.ML HOL-Nominal Slides |
|
202 |
|
203 slidesA: sessionA |
|
204 rm -f Slides/generatedA/*.aux # otherwise latex will fall over |
|
205 cd Slides/generatedA ; $(ISABELLE_TOOL) latex -o pdf root.beamer.tex |
|
206 cd Slides/generatedA ; $(ISABELLE_TOOL) latex -o pdf root.beamer.tex |
|
207 cp Slides/generatedA/root.beamer.pdf Slides/slidesA.pdf |
|
208 |
|
209 slides: slides1 slides2 slides3 slides4 slides5 slides6 slides7 slides8 slides8 slides9 slidesA |
200 |
210 |
201 |
211 |
202 |
212 |
203 |
213 |
204 ## clean |
214 ## clean |