--- a/IsaMakefile	Wed Aug 29 13:05:25 2012 +0000
+++ b/IsaMakefile	Wed Aug 29 13:05:46 2012 +0000
@@ -24,7 +24,7 @@
 slides1: session1 
 	rm -f Slides/generated/*.aux # otherwise latex will fall over
 	cd Slides/generated ; $(ISABELLE_TOOL) latex -o pdf root.beamer.tex 
-	cp Slides/generated/root.beamer.pdf Slides/slides.pdf     
+	cp Slides/generated/root.beamer.pdf Slides/slides1.pdf     
 
 ## Slides 2
 
@@ -36,7 +36,7 @@
 slides2: session2 
 	rm -f Slides/generated/*.aux # otherwise latex will fall over
 	cd Slides/generated ; $(ISABELLE_TOOL) latex -o pdf root.beamer.tex 
-	cp Slides/generated/root.beamer.pdf Slides/slides1.pdf   
+	cp Slides/generated/root.beamer.pdf Slides/slides2.pdf   
 
 ## Slides 3
 
@@ -48,13 +48,13 @@
 slides3: session3 
 	rm -f Slides/generated/*.aux # otherwise latex will fall over
 	cd Slides/generated ; $(ISABELLE_TOOL) latex -o pdf root.beamer.tex 
-	cp Slides/generated/root.beamer.pdf Slides/slides2.pdf   
+	cp Slides/generated/root.beamer.pdf Slides/slides3.pdf   
 
 ## Slides 4
 
 session4: Slides/ROOT.ML \
          Slides/document/root* \
-         Slides/Slides2.thy
+         Slides/Slides4.thy
 	@$(USEDIR) -D generated -f ROOT4.ML HOL Slides
 
 slides4: session4 
@@ -62,8 +62,21 @@
 	cd Slides/generated ; $(ISABELLE_TOOL) latex -o pdf root.beamer.tex 
 	cp Slides/generated/root.beamer.pdf Slides/slides4.pdf  
 
+## Slides 5
 
-slides: slides1 slides2 slides3 slides4
+session5: Slides/ROOT.ML \
+         Slides/document/root* \
+         Slides/Slides5.thy
+	@$(USEDIR) -D generated -f ROOT5.ML HOL Slides
+
+slides5: session5 
+	rm -f Slides/generated/*.aux # otherwise latex will fall over
+	cd Slides/generated ; $(ISABELLE_TOOL) latex -o pdf root.beamer.tex 
+	cp Slides/generated/root.beamer.pdf Slides/slides5.pdf  
+
+
+
+slides: slides1 slides2 slides3 slides4 slides5
 
 
 ## ITP itp