diff -r a06de111c70e -r 41ec301eb062 IsaMakefile
--- a/IsaMakefile	Sat Nov 26 09:44:34 2011 +0000
+++ b/IsaMakefile	Sat Nov 26 09:47:21 2011 +0000
@@ -168,7 +168,19 @@
 	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
+session9: Slides/ROOT9.ML \
+         Slides/document/root* \
+         Slides/Slides6.thy
+	@$(USEDIR) -D generated9 -f ROOT9.ML HOL-Nominal Slides
+
+slides9: session9
+	rm -f Slides/generated9/*.aux # otherwise latex will fall over                                      
+	cd Slides/generated9 ; $(ISABELLE_TOOL) latex -o pdf root.beamer.tex
+	cd Slides/generated9 ; $(ISABELLE_TOOL) latex -o pdf root.beamer.tex
+	cp Slides/generated9/root.beamer.pdf Slides/slides9.pdf 
+
+
+slides: slides1 slides2 slides3 slides4 slides5 slides6 slides7 slides8 slides8