--- a/IsaMakefile	Wed Mar 16 21:14:43 2011 +0100
+++ b/IsaMakefile	Tue Mar 29 23:52:14 2011 +0200
@@ -4,7 +4,7 @@
 default: tests
 images: 
 
-all: tests paper pearl pearl-jv qpaper slides
+all: tests esop pearl pearl-jv qpaper slides
 
 
 ## global settings
@@ -23,15 +23,14 @@
 $(LOG)/HOL-Nominal2.gz: Nominal/ROOT.ML Nominal/*.thy
 	@cd Nominal; $(USEDIR) -b -d "" HOL Nominal
 
-## Nominal2 Paper
+## ESOP Paper
 
-paper: $(LOG)/HOL-Nominal2-Paper.gz
+esop: $(LOG)/HOL-ESOP-Paper.gz
 
-$(LOG)/HOL-Nominal2-Paper.gz: Paper/ROOT.ML Paper/document/root.* Paper/*.thy
-	@$(USEDIR) -f ROOTa.ML -D generated HOL Paper
-	@$(USEDIR) -D generated HOL Paper
-	$(ISABELLE_TOOL) document -o pdf  Paper/generated
-	@cp Paper/document.pdf paper.pdf
+$(LOG)/HOL-ESOP-Paper.gz: ESOP-Paper/ROOT.ML ESOP-Paper/document/root.* ESOP-Paper/*.thy
+	@$(USEDIR) -f ROOT.ML -D generated HOL-Nominal2 ESOP-Paper
+	$(ISABELLE_TOOL) document -o pdf  ESOP-Paper/generated
+	@cp ESOP-Paper/document.pdf esop-paper.pdf
 
 ## Pearl Paper ITP
 
@@ -107,7 +106,18 @@
 	cd Slides/generated4 ; $(ISABELLE_TOOL) latex -o pdf root.beamer.tex
 	cp Slides/generated4/root.beamer.pdf Slides/slides4.pdf 
 
-slides: slides1 slides2 slides3 slides4
+session5: Slides/ROOT5.ML \
+         Slides/document/root* \
+         Slides/Slides5.thy
+	@$(USEDIR) -D generated5 -f ROOT5.ML HOL-Nominal Slides
+
+slides5: session5
+	rm -f Slides/generated5/*.aux # otherwise latex will fall over
+	cd Slides/generated5 ; $(ISABELLE_TOOL) latex -o pdf root.beamer.tex
+	cd Slides/generated5 ; $(ISABELLE_TOOL) latex -o pdf root.beamer.tex
+	cp Slides/generated5/root.beamer.pdf Slides/slides5.pdf 
+
+slides: slides1 slides2 slides3 slides4 slides5