--- a/IsaMakefile	Thu Jan 17 11:51:00 2013 +0000
+++ b/IsaMakefile	Fri Jan 18 11:40:01 2013 +0000
@@ -32,6 +32,19 @@
 	$(ISABELLE_TOOL) document -o pdf  generated
 	cp generated/root.pdf paper.pdf  
 
+## ITP itp
+
+session_itp: Paper/ROOT.ML \
+	Paper/document/root* \
+	Paper/*.thy
+	@$(USEDIR) -D generated -f ROOT.ML HOL Paper
+
+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
+	cd Paper/generated ; $(ISABELLE_TOOL) latex -o pdf root.tex
+	cp Paper/generated/root.pdf paper.pdf   
 
 ## clean