diff -r 5faa1b59e870 -r 813e7257c7c3 IsaMakefile
--- a/IsaMakefile	Thu Feb 16 08:12:01 2012 +0000
+++ b/IsaMakefile	Mon Feb 20 11:02:50 2012 +0000
@@ -14,78 +14,54 @@
 USEDIR = $(ISABELLE_TOOL) usedir -v true -t true 
 
 
-## Slides
+## Slides 1
 
 session1: Slides/ROOT.ML \
          Slides/document/root* \
          Slides/Slides.thy
 	@$(USEDIR) -D generated -f ROOT.ML HOL Slides
 
-slides: session1 
+slides1: 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     
 
-## Slides 1
+## Slides 2
 
-session11: Slides/ROOT.ML \
+session2: Slides/ROOT.ML \
          Slides/document/root* \
          Slides/Slides1.thy
 	@$(USEDIR) -D generated -f ROOT1.ML HOL Slides
 
-slides1: session11 
+slides2: session2 
 	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/slides1.pdf   
 
-## Slides 2
+## Slides 3
 
-session22: Slides/ROOT.ML \
+session3: Slides/ROOT.ML \
          Slides/document/root* \
          Slides/Slides2.thy
 	@$(USEDIR) -D generated -f ROOT2.ML HOL Slides
 
-slides2: session22 
+slides3: session3 
 	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/slides2.pdf   
 
-## long paper
 
-session2: tphols-2011/ROOT.ML \
-         tphols-2011/document/root* \
-         *.thy
-	@$(USEDIR) -D generated -f ROOT.ML ListP tphols-2011 
-
-paper: session2 
-	rm -f tphols-2011/generated/*.aux # otherwise latex will fall over
-	cd tphols-2011/generated ; $(ISABELLE_TOOL) latex -o pdf root.tex 
-	cd tphols-2011/generated ; $(ISABELLE_TOOL) latex -o pdf root.tex 
-	cp tphols-2011/generated/root.pdf tphols-2011/myhill.pdf     
-
-## full paper
-
-fullsession2: tphols-2011/ROOT.ML \
-         tphols-2011/document/root* \
-         *.thy
-	@$(USEDIR) -D generated -f ROOT.ML HOL tphols-2011 
-
-fullpaper: fullsession2 
-	rm -f tphols-2011/generated/*.aux # otherwise latex will fall over
-	cd tphols-2011/generated ; $(ISABELLE_TOOL) latex -o pdf root.tex 
-	cd tphols-2011/generated ; $(ISABELLE_TOOL) latex -o pdf root.tex 
-	cp tphols-2011/generated/root.pdf tphols-2011/myhill.pdf   
-
+slides: slides1 slides2 slides3
 
 
 ## ITP paper
 
-session3: Paper/ROOT.ML \
+session_itp: Paper/ROOT.ML \
 	Paper/document/root* \
 	Paper/*.thy
 	@$(USEDIR) -D generated -f ROOT.ML HOL Paper
 
-itp: session3
+itp: session_itp
 	rm -f Paper/generated/*.aux # otherwise latex will fall over      
 	cd Paper/generated ; $(ISABELLE_TOOL) latex -o pdf root.tex 
 	cd Paper/generated ; bibtex root
@@ -94,12 +70,12 @@
 
 ## Journal Version
 
-session4: Journal/ROOT.ML \
+session_journal: Journal/ROOT.ML \
 	Journal/document/root* \
 	Journal/*.thy
 	@$(USEDIR) -D generated -f ROOT.ML HOL Journal
 
-journal: session4
+journal: session_journal
 	rm -f Journal/generated/*.aux # otherwise latex will fall over       
 	cd Journal/generated ; $(ISABELLE_TOOL) latex -o pdf root.tex 
 	cd Journal/generated ; bibtex root
@@ -110,5 +86,6 @@
 ## clean
 
 clean:
-	rm -rf Slides/generated/*
-	rm -rf tphols-2011/generated/*
+	rm -rf Slides/generated*
+	rm -rf Paper/generated*
+	rm -rf Journal/generated*