diff -r d2ddce8b36fd -r f5cc33a0ba99 IsaMakefile
--- a/IsaMakefile	Wed Jan 26 22:23:56 2011 +0000
+++ b/IsaMakefile	Wed Jan 26 22:51:51 2011 +0000
@@ -27,19 +27,34 @@
 	cp Slides/generated/root.beamer.pdf Slides/slides.pdf     
 
 
-## Paper
+## long paper
 
 session2: tphols-2011/ROOT.ML \
          tphols-2011/document/root* \
          *.thy
-	@$(USEDIR) -D generated -f ROOT.ML ListP tphols-2011 
+	@$(USEDIR) -D generated -f ROOT.ML HOL 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     
 
 
+## ITP paper
+
+session3: Paper/ROOT.ML \
+	Paper/document/root* \
+	Paper/*.thy
+	@$(USEDIR) -D generated -f ROOT.ML HOL Paper
+
+itp: session3
+	rm -f Paper/generated/*.aux # otherwise latex will fall over      
+	cd Paper/generated ; $(ISABELLE_TOOL) latex -o pdf root.tex 
+	cd Paper/generated ; $(ISABELLE_TOOL) latex -o pdf root.tex
+	cp Paper/generated/root.pdf paper.pdf     
+
+
 ## clean
 
 clean: