equal
deleted
inserted
replaced
126 rm -f Slides/generated6/*.aux # otherwise latex will fall over |
126 rm -f Slides/generated6/*.aux # otherwise latex will fall over |
127 cd Slides/generated6 ; $(ISABELLE_TOOL) latex -o pdf root.beamer.tex |
127 cd Slides/generated6 ; $(ISABELLE_TOOL) latex -o pdf root.beamer.tex |
128 cd Slides/generated6 ; $(ISABELLE_TOOL) latex -o pdf root.beamer.tex |
128 cd Slides/generated6 ; $(ISABELLE_TOOL) latex -o pdf root.beamer.tex |
129 cp Slides/generated6/root.beamer.pdf Slides/slides6.pdf |
129 cp Slides/generated6/root.beamer.pdf Slides/slides6.pdf |
130 |
130 |
131 slides: slides1 slides2 slides3 slides4 slides5 slides6 |
131 session7: Slides/ROOT7.ML \ |
|
132 Slides/document/root* \ |
|
133 Slides/Slides6.thy |
|
134 @$(USEDIR) -D generated7 -f ROOT7.ML HOL Slides |
|
135 |
|
136 slides7: session7 |
|
137 rm -f Slides/generated7/*.aux # otherwise latex will fall over |
|
138 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 |
|
141 |
|
142 |
|
143 slides: slides1 slides2 slides3 slides4 slides5 slides6 slides7 |
132 |
144 |
133 |
145 |
134 |
146 |
135 |
147 |
136 ## clean |
148 ## clean |