diff -r 813e7257c7c3 -r d47c2143ab8a IsaMakefile
--- a/IsaMakefile	Mon Feb 20 11:02:50 2012 +0000
+++ b/IsaMakefile	Wed Feb 22 13:25:49 2012 +0000
@@ -1,8 +1,8 @@
 
 ## targets
 
-default: paper
-all: slides paper
+default: slides4
+all: slides itp
 
 ## global settings
 
@@ -50,11 +50,23 @@
 	cd Slides/generated ; $(ISABELLE_TOOL) latex -o pdf root.beamer.tex 
 	cp Slides/generated/root.beamer.pdf Slides/slides2.pdf   
 
+## Slides 4
 
-slides: slides1 slides2 slides3
+session4: Slides/ROOT.ML \
+         Slides/document/root* \
+         Slides/Slides2.thy
+	@$(USEDIR) -D generated -f ROOT4.ML HOL Slides
+
+slides4: session4 
+	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/slides4.pdf  
 
 
-## ITP paper
+slides: slides1 slides2 slides3 slides4
+
+
+## ITP itp
 
 session_itp: Paper/ROOT.ML \
 	Paper/document/root* \