--- a/IsaMakefile	Wed Mar 17 17:11:23 2010 +0100
+++ b/IsaMakefile	Wed Mar 17 20:42:22 2010 +0100
@@ -4,7 +4,7 @@
 default: Nominal2
 images: 
 
-all: Nominal2
+all: Nominal2 paper
 
 
 ## global settings
@@ -21,12 +21,12 @@
 Nominal2: $(LOG)/HOL-Nominal2.gz
 
 $(LOG)/HOL-Nominal2.gz: Nominal/ROOT.ML Nominal/*.thy
-	@$(USEDIR) HOL Nominal
+	@cd Nominal; $(USEDIR) -b -d "" HOL Nominal
 
 paper: $(LOG)/HOL-Nominal2-Paper.gz
 
 $(LOG)/HOL-Nominal2-Paper.gz: Paper/ROOT.ML Paper/document/root.tex Paper/*.thy
-	@$(USEDIR) -D generated HOL Paper
+	@$(USEDIR) -D generated Nominal Paper
 	$(ISABELLE_TOOL) document -o pdf  Paper/generated
 	@cp Paper/document.pdf paper.pdf
 

--- a/Paper/Paper.thy	Wed Mar 17 17:11:23 2010 +0100
+++ b/Paper/Paper.thy	Wed Mar 17 20:42:22 2010 +0100
@@ -16,17 +16,18 @@
   definition given by Leroy in [] is incorrect (it omits a
   side-condition).
 
-  Examples: type-schemes
+  Examples: type-schemes, Spi-calculus
 
   Contributions:  We provide definitions for when terms
   involving general bindings are alpha-equivelent.
 *}
 
-text {* A Brief Overview about the Nominal Logic Work *}
+section {* A Brief Overview about the Nominal Logic Work *}
 
-text {* Abstractions *}
+section {* Abstractions *}
 
-text {* Alpha-Equivalence and Free Variables *}
+section {* Alpha-Equivalence and Free Variables *}
+
 
 
 text {*

--- a/Paper/ROOT.ML	Wed Mar 17 17:11:23 2010 +0100
+++ b/Paper/ROOT.ML	Wed Mar 17 20:42:22 2010 +0100
@@ -1,3 +1,2 @@
 quick_and_dirty := true;
-no_document use_thys ["../Nominal/Test"];
 use_thys ["Paper"];
\ No newline at end of file