diff -r 64a03564bc24 -r 1a1a2b778ba2 IsaMakefile
--- 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