diff -r e31b733ace44 -r f72c82bf59e5 IsaMakefile
--- a/IsaMakefile	Thu Nov 18 11:39:17 2010 +0000
+++ b/IsaMakefile	Thu Nov 25 18:54:45 2010 +0000
@@ -1,8 +1,8 @@
 
 ## targets
 
-default: slides
-all: slides 
+default: paper
+all: slides paper
 
 ## global settings
 
@@ -12,22 +12,36 @@
 
 
 USEDIR = $(ISABELLE_TOOL) usedir -v true -t true 
+
+
 ## Slides
 
-session1: Slides/ROOT1.ML \
+session1: Slides/ROOT.ML \
          Slides/document/root* \
-         Slides/Slides1.thy
-	@$(USEDIR) -D generated1 -f ROOT1.ML HOL Slides
+         Slides/Slides.thy
+	@$(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     
+
 
-slides1: session1 
-	rm -f Slides/generated1/*.aux # otherwise latex will fall over
-	cd Slides/generated1 ; $(ISABELLE_TOOL) latex -o pdf root.beamer.tex 
-	cp Slides/generated1/root.beamer.pdf Slides/slides.pdf     
+## Paper
 
-slides: slides1 
+session2: Paper/ROOT.ML \
+         Paper/document/root* \
+         Paper/Paper.thy
+	@$(USEDIR) -D generated -f ROOT.ML HOL Paper
+
+paper: session2 
+	rm -f Paper/generated/*.aux # otherwise latex will fall over
+	cd Paper/generated ; $(ISABELLE_TOOL) latex -o pdf root.tex 
+	cp Paper/generated/root.pdf Paper/paper.pdf     
 
 
 ## clean
 
 clean:
-	rm -rf Slides/generated1/*
+	rm -rf Slides/generated/*
+	rm -rf Paper/generated/*