diff -r 368fc38321fc -r 878de0084b62 IsaMakefile
--- a/IsaMakefile	Thu Feb 16 07:14:28 2012 +0000
+++ b/IsaMakefile	Fri Feb 17 02:05:00 2012 +0000
@@ -195,8 +195,18 @@
 	cd Slides/generated9 ; $(ISABELLE_TOOL) latex -o pdf root.beamer.tex
 	cp Slides/generated9/root.beamer.pdf Slides/slides9.pdf 
 
+sessionA: Slides/ROOTA.ML \
+	Slides/document/root* \
+	Slides/SlidesA.thy
+	@$(USEDIR) -D generatedA -f ROOTA.ML HOL-Nominal Slides
 
-slides: slides1 slides2 slides3 slides4 slides5 slides6 slides7 slides8 slides8 slides9
+slidesA: sessionA
+	rm -f Slides/generatedA/*.aux # otherwise latex will fall over
+	cd Slides/generatedA ; $(ISABELLE_TOOL) latex -o pdf root.beamer.tex
+	cd Slides/generatedA ; $(ISABELLE_TOOL) latex -o pdf root.beamer.tex
+	cp Slides/generatedA/root.beamer.pdf Slides/slidesA.pdf 
+
+slides: slides1 slides2 slides3 slides4 slides5 slides6 slides7 slides8 slides8 slides9 slidesA