--- a/IsaMakefile	Sat May 14 10:16:16 2011 +0100
+++ b/IsaMakefile	Sun May 22 10:20:18 2011 +0200
@@ -139,8 +139,18 @@
 	cd Slides/generated7 ; $(ISABELLE_TOOL) latex -o pdf root.beamer.tex
 	cp Slides/generated7/root.beamer.pdf Slides/slides7.pdf 
 
+session8: Slides/ROOT8.ML \
+         Slides/document/root* \
+         Slides/Slides6.thy
+	@$(USEDIR) -D generated8 -f ROOT8.ML HOL Slides
 
-slides: slides1 slides2 slides3 slides4 slides5 slides6 slides7
+slides8: session8
+	rm -f Slides/generated8/*.aux # otherwise latex will fall over                                      
+	cd Slides/generated8 ; $(ISABELLE_TOOL) latex -o pdf root.beamer.tex
+	cd Slides/generated8 ; $(ISABELLE_TOOL) latex -o pdf root.beamer.tex
+	cp Slides/generated8/root.beamer.pdf Slides/slides8.pdf 
+
+slides: slides1 slides2 slides3 slides4 slides5 slides6 slides7 slides8