diff -r 66ef2a2c64fb -r c3ff26204d2a IsaMakefile
--- a/IsaMakefile	Fri Apr 22 00:18:25 2011 +0800
+++ b/IsaMakefile	Thu Apr 28 11:44:36 2011 +0800
@@ -128,7 +128,19 @@
 	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
+session7: Slides/ROOT7.ML \
+         Slides/document/root* \
+         Slides/Slides6.thy
+	@$(USEDIR) -D generated7 -f ROOT7.ML HOL Slides
+
+slides7: session7
+	rm -f Slides/generated7/*.aux # otherwise latex will fall over                                      
+	cd Slides/generated7 ; $(ISABELLE_TOOL) latex -o pdf root.beamer.tex
+	cd Slides/generated7 ; $(ISABELLE_TOOL) latex -o pdf root.beamer.tex
+	cp Slides/generated7/root.beamer.pdf Slides/slides7.pdf 
+
+
+slides: slides1 slides2 slides3 slides4 slides5 slides6 slides7