# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1268854962 -3600
# Node ID 4908db645f989100251da3073932943de87b6d89
# Parent  f970ca9b5bec4c81fc4e8d37085c77c17fa18dae# Parent  9923b2cee778496a649ad17bb074d1aab379d006
merged

diff -r 9923b2cee778 -r 4908db645f98 IsaMakefile
--- a/IsaMakefile	Wed Mar 17 18:53:23 2010 +0100
+++ b/IsaMakefile	Wed Mar 17 20:42:42 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
 
diff -r 9923b2cee778 -r 4908db645f98 Paper/Paper.thy
--- a/Paper/Paper.thy	Wed Mar 17 18:53:23 2010 +0100
+++ b/Paper/Paper.thy	Wed Mar 17 20:42:42 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 {*
diff -r 9923b2cee778 -r 4908db645f98 Paper/ROOT.ML
--- a/Paper/ROOT.ML	Wed Mar 17 18:53:23 2010 +0100
+++ b/Paper/ROOT.ML	Wed Mar 17 20:42:42 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