diff -r 1af453d56083 -r e36beb11723c IsaMakefile
--- a/IsaMakefile	Wed Jun 15 11:06:48 2011 +0900
+++ b/IsaMakefile	Wed Jun 15 12:32:40 2011 +0100
@@ -60,6 +60,15 @@
 	$(ISABELLE_TOOL) document -o pdf Quotient-Paper/generated
 	@cp Quotient-Paper/document.pdf qpaper.pdf
 
+## Nominal Functions paper
+
+fnpaper: $(LOG)/HOL-FnPaper.gz
+
+$(LOG)/HOL-FnPaper.gz: Fun-Paper/ROOT.ML Fun-Paper/document/root.* Fun-Paper/*.thy
+	@$(USEDIR) -D generated HOL Fun-Paper
+	$(ISABELLE_TOOL) document -o pdf Fun-Paper/generated
+	@cp Fun-Paper/document.pdf fnpaper.pdf
+
 ## Slides
 
 session1: Slides/ROOT1.ML \