diff -r 4cf3a4d36799 -r 9876d73adb2b IsaMakefile
--- a/IsaMakefile	Tue May 22 14:00:59 2012 +0200
+++ b/IsaMakefile	Tue May 22 14:55:58 2012 +0200
@@ -86,6 +86,26 @@
 	$(ISABELLE_TOOL) document -o pdf Quotient-Paper-jv/generated
 	@cp Quotient-Paper-jv/document.pdf qpaper-jv.pdf
 
+## SFT Paper
+
+sft-paper: $(LOG)/Nominal-SFT-Paper.gz
+
+$(LOG)/Nominal-SFT-Paper.gz: Nominal/Ex/SFT/ROOT.ML Nominal/Ex/SFT/document/root.* Nominal/Ex/SFT/*.thy
+	@$(USEDIR) -f ROOT.ML -D generated Nominal2 Nominal/Ex/SFT
+	$(ISABELLE_TOOL) document -o pdf  Nominal/Ex/SFT/generated
+	@cp Nominal/Ex/SFT/document.pdf sft-paper.pdf
+
+
+## Exec Paper
+
+exec-paper: $(LOG)/Nominal-Exec-Paper.gz
+
+$(LOG)/Nominal-Exec-Paper.gz: Nominal/Ex/Exec/ROOT.ML Nominal/Ex/Exec/document/root.* Nominal/Ex/Exec/*.thy
+	@$(USEDIR) -f ROOT.ML -D generated Nominal2 Nominal/Ex/Exec
+	$(ISABELLE_TOOL) document -o pdf  Nominal/Ex/Exec/generated
+	@cp Nominal/Ex/Exec/document.pdf exec-paper.pdf
+
+
 ## Nominal Functions paper
 
 fnpaper: $(LOG)/HOL-FnPaper.gz