diff -r 0a5320c6a7e6 -r 842969a598f2 IsaMakefile
--- a/IsaMakefile	Fri Jul 09 23:04:51 2010 +0100
+++ b/IsaMakefile	Sat Jul 10 11:27:04 2010 +0100
@@ -62,20 +62,38 @@
 
 ## Slides
 
-session1: Slides/ROOT.ML \
+session1: Slides/ROOT1.ML \
          Slides/document/root* \
          Slides/Slides1.thy
-	@$(USEDIR) -D generated1 -f ROOT.ML HOL-Nominal Slides
-	@perl -i -p -e "s/..isachardoublequoteopen./\\\begin{innerdouble}/g" Sl
-	@perl -i -p -e "s/..isachardoublequoteclose./\\\end{innerdouble}/g" Sli
-	@perl -i -p -e "s/..isacharbackquoteopen./\\\begin{innersingle}/g" Slid
-	@perl -i -p -e "s/..isacharbackquoteclose./\\\end{innersingle}/g" Slide
+	@$(USEDIR) -D generated1 -f ROOT1.ML HOL-Nominal Slides
 
 slides1: session1
 	rm -f Slides/generated1/*.aux # otherwise latex will fall over
 	cd Slides/generated1 ; $(ISABELLE_TOOL) latex -o pdf root.beamer.tex
 	cd Slides/generated1 ; $(ISABELLE_TOOL) latex -o pdf root.beamer.tex
-	cp Slides/generated1/root.beamer.pdf Slides/slides.pdf     
+	cp Slides/generated1/root.beamer.pdf Slides/slides1.pdf     
+
+session2: Slides/ROOT2.ML \
+         Slides/document/root* \
+         Slides/Slides2.thy
+	@$(USEDIR) -D generated2 -f ROOT2.ML HOL-Nominal Slides
+
+slides2: session2
+	rm -f Slides/generated2/*.aux # otherwise latex will fall over
+	cd Slides/generated2 ; $(ISABELLE_TOOL) latex -o pdf root.beamer.tex
+	cd Slides/generated2 ; $(ISABELLE_TOOL) latex -o pdf root.beamer.tex
+	cp Slides/generated2/root.beamer.pdf Slides/slides2.pdf 
+
+session3: Slides/ROOT3.ML \
+         Slides/document/root* \
+         Slides/Slides3.thy
+	@$(USEDIR) -D generated3 -f ROOT3.ML HOL-Nominal Slides
+
+slides3: session3
+	rm -f Slides/generated3/*.aux # otherwise latex will fall over
+	cd Slides/generated3 ; $(ISABELLE_TOOL) latex -o pdf root.beamer.tex
+	cd Slides/generated3 ; $(ISABELLE_TOOL) latex -o pdf root.beamer.tex
+	cp Slides/generated3/root.beamer.pdf Slides/slides3.pdf 
 
 slides: slides1