diff -r aa8656a8dbef -r 4b9aa15ff713 IsaMakefile
--- a/IsaMakefile	Mon Dec 24 01:26:23 2012 +0000
+++ b/IsaMakefile	Wed Dec 26 14:52:14 2012 +0000
@@ -14,15 +14,27 @@
 OUT = $(ISABELLE_OUTPUT)
 LOG = $(OUT)/log
 
-USEDIR = $(ISABELLE_TOOL) usedir -v true -i true -d pdf  ## -D generated
+USEDIR = $(ISABELLE_TOOL) usedir -v true -i false -d pdf  ## -D generated
 
 
 ## utm
 
 utm: $(OUT)/utm
 
-$(OUT)/utm: ## ROOT.ML document/root.tex *.thy
-	@$(USEDIR) -b HOL utm
+$(OUT)/utm: *.thy
+	@$(USEDIR) -b HOL UTM
+
+session:  ROOT.ML \
+	document/root* \
+	*.thy
+	@$(USEDIR) -D generated -f ROOT.ML UTM .
+
+paper: utm
+	rm -f generated/*.aux # otherwise latex will fall over       
+	cd generated ; $(ISABELLE_TOOL) latex -o pdf root.tex 
+#	cd generated ; bibtex root
+#	cd generated ; $(ISABELLE_TOOL) latex -o pdf root.tex
+	cp generated/root.pdf paper.pdf  
 
 
 ## clean