--- a/IsaMakefile	Mon May 24 21:11:33 2010 +0100
+++ b/IsaMakefile	Tue May 25 00:24:41 2010 +0100
@@ -60,6 +60,27 @@
 	$(ISABELLE_TOOL) document -o pdf Quotient-Paper/generated
 	@cp Quotient-Paper/document.pdf qpaper.pdf
 
+## Slides
+
+session1: Slides/ROOT.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
+
+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     
+
+slides: slides1
+
+
+
 
 ## clean