diff -r 670131bcba4a -r b85875d65b10 IsaMakefile
--- a/IsaMakefile	Tue Dec 15 15:38:17 2009 +0100
+++ b/IsaMakefile	Wed Dec 16 14:08:42 2009 +0100
@@ -13,14 +13,21 @@
 OUT = $(ISABELLE_OUTPUT)
 LOG = $(OUT)/log
 
-USEDIR = $(ISABELLE_TOOL) usedir -v true -t true ## -D generated
+USEDIR = $(ISABELLE_TOOL) usedir -v true -t true -D generated
 
 ## Quot
 
 Quot: $(LOG)/HOL-Quot.gz
 
 $(LOG)/HOL-Quot.gz: Quot/ROOT.ML Quot/*.thy
-	@$(USEDIR) HOL-Nominal Quot
+	@$(USEDIR) HOL-Quot Quot
+
+paper: $(LOG)/HOL-Quot-Paper.gz
+
+$(LOG)/HOL-Quot-Paper.gz: Paper/ROOT.ML Paper/document/root.tex Paper/*.thy
+	@$(USEDIR) HOL Paper
+	$(ISATOOL) document -o pdf  Paper/generated
+	@cp Paper/document.pdf paper.pdf
 
 
 ## clean