diff -r 0bc1db726f81 -r ac3470e1e5af IsaMakefile
--- a/IsaMakefile	Mon Aug 30 11:02:13 2010 +0900
+++ b/IsaMakefile	Tue Aug 31 21:03:08 2010 +0800
@@ -95,7 +95,18 @@
 	cd Slides/generated3 ; $(ISABELLE_TOOL) latex -o pdf root.beamer.tex
 	cp Slides/generated3/root.beamer.pdf Slides/slides3.pdf 
 
-slides: slides1
+session4: Slides/ROOT4.ML \
+         Slides/document/root* \
+         Slides/Slides4.thy
+	@$(USEDIR) -D generated4 -f ROOT4.ML HOL-Nominal Slides
+
+slides4: session4
+	rm -f Slides/generated4/*.aux # otherwise latex will fall over
+	cd Slides/generated4 ; $(ISABELLE_TOOL) latex -o pdf root.beamer.tex
+	cd Slides/generated4 ; $(ISABELLE_TOOL) latex -o pdf root.beamer.tex
+	cp Slides/generated4/root.beamer.pdf Slides/slides4.pdf 
+
+slides: slides4