diff -r 09e6f3719cbc -r 5d724fe0e096 IsaMakefile
--- a/IsaMakefile	Fri Aug 19 20:39:07 2011 +0000
+++ b/IsaMakefile	Mon Aug 22 12:49:27 2011 +0000
@@ -19,13 +19,25 @@
 session1: Slides/ROOT.ML \
          Slides/document/root* \
          Slides/Slides.thy
-	@$(USEDIR) -D generated -f ROOT.ML ListP tphols-2011 
+	@$(USEDIR) -D generated -f ROOT.ML HOL Slides
 
 slides: 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     
 
+## Slides
+
+session11: Slides/ROOT.ML \
+         Slides/document/root* \
+         Slides/Slides1.thy
+	@$(USEDIR) -D generated -f ROOT1.ML HOL Slides
+
+slides1: session11 
+	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   
+
 
 ## long paper