equal
deleted
inserted
replaced
137 rm -f Slides/generated7/*.aux # otherwise latex will fall over |
137 rm -f Slides/generated7/*.aux # otherwise latex will fall over |
138 cd Slides/generated7 ; $(ISABELLE_TOOL) latex -o pdf root.beamer.tex |
138 cd Slides/generated7 ; $(ISABELLE_TOOL) latex -o pdf root.beamer.tex |
139 cd Slides/generated7 ; $(ISABELLE_TOOL) latex -o pdf root.beamer.tex |
139 cd Slides/generated7 ; $(ISABELLE_TOOL) latex -o pdf root.beamer.tex |
140 cp Slides/generated7/root.beamer.pdf Slides/slides7.pdf |
140 cp Slides/generated7/root.beamer.pdf Slides/slides7.pdf |
141 |
141 |
|
142 session8: Slides/ROOT8.ML \ |
|
143 Slides/document/root* \ |
|
144 Slides/Slides6.thy |
|
145 @$(USEDIR) -D generated8 -f ROOT8.ML HOL Slides |
142 |
146 |
143 slides: slides1 slides2 slides3 slides4 slides5 slides6 slides7 |
147 slides8: session8 |
|
148 rm -f Slides/generated8/*.aux # otherwise latex will fall over |
|
149 cd Slides/generated8 ; $(ISABELLE_TOOL) latex -o pdf root.beamer.tex |
|
150 cd Slides/generated8 ; $(ISABELLE_TOOL) latex -o pdf root.beamer.tex |
|
151 cp Slides/generated8/root.beamer.pdf Slides/slides8.pdf |
|
152 |
|
153 slides: slides1 slides2 slides3 slides4 slides5 slides6 slides7 slides8 |
144 |
154 |
145 |
155 |
146 |
156 |
147 |
157 |
148 ## clean |
158 ## clean |