equal
deleted
inserted
replaced
115 rm -f Slides/generated5/*.aux # otherwise latex will fall over |
115 rm -f Slides/generated5/*.aux # otherwise latex will fall over |
116 cd Slides/generated5 ; $(ISABELLE_TOOL) latex -o pdf root.beamer.tex |
116 cd Slides/generated5 ; $(ISABELLE_TOOL) latex -o pdf root.beamer.tex |
117 cd Slides/generated5 ; $(ISABELLE_TOOL) latex -o pdf root.beamer.tex |
117 cd Slides/generated5 ; $(ISABELLE_TOOL) latex -o pdf root.beamer.tex |
118 cp Slides/generated5/root.beamer.pdf Slides/slides5.pdf |
118 cp Slides/generated5/root.beamer.pdf Slides/slides5.pdf |
119 |
119 |
120 slides: slides1 slides2 slides3 slides4 slides5 |
120 session6: Slides/ROOT6.ML \ |
|
121 Slides/document/root* \ |
|
122 Slides/Slides6.thy |
|
123 @$(USEDIR) -D generated6 -f ROOT6.ML HOL-Nominal Slides |
|
124 |
|
125 slides6: session6 |
|
126 rm -f Slides/generated6/*.aux # otherwise latex will fall over |
|
127 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 |
|
130 |
|
131 slides: slides1 slides2 slides3 slides4 slides5 slides6 |
121 |
132 |
122 |
133 |
123 |
134 |
124 |
135 |
125 ## clean |
136 ## clean |