Mercurial Mercurial > hg > nominal2 / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
IsaMakefile
changeset 2762 1a1a2b778ba2
parent 2749 7cf2d79d8d5e
child 2772 c3ff26204d2a 
--- a/IsaMakefile	Sun Apr 10 14:13:55 2011 +0800
+++ b/IsaMakefile	Mon Apr 11 02:04:11 2011 +0100
@@ -117,7 +117,18 @@
 	cd Slides/generated5 ; $(ISABELLE_TOOL) latex -o pdf root.beamer.tex
 	cp Slides/generated5/root.beamer.pdf Slides/slides5.pdf 
 
-slides: slides1 slides2 slides3 slides4 slides5
+session6: Slides/ROOT6.ML \
+         Slides/document/root* \
+         Slides/Slides6.thy
+	@$(USEDIR) -D generated6 -f ROOT6.ML HOL-Nominal Slides
+
+slides6: session6
+	rm -f Slides/generated6/*.aux # otherwise latex will fall over
+	cd Slides/generated6 ; $(ISABELLE_TOOL) latex -o pdf root.beamer.tex
+	cd Slides/generated6 ; $(ISABELLE_TOOL) latex -o pdf root.beamer.tex
+	cp Slides/generated6/root.beamer.pdf Slides/slides6.pdf 
+
+slides: slides1 slides2 slides3 slides4 slides5 slides6
nominal2