--- a/IsaMakefile	Sun Apr 04 21:39:28 2010 +0200
+++ b/IsaMakefile	Tue Apr 06 07:36:15 2010 +0200
@@ -27,7 +27,7 @@
 
 paper: $(LOG)/HOL-Nominal2-Paper.gz
 
-$(LOG)/HOL-Nominal2-Paper.gz: Paper/ROOT.ML Paper/document/root.tex Paper/*.thy
+$(LOG)/HOL-Nominal2-Paper.gz: Paper/ROOT.ML Paper/document/root.* Paper/*.thy
 	@$(USEDIR) -D generated Nominal Paper
 	$(ISABELLE_TOOL) document -o pdf  Paper/generated
 	@cp Paper/document.pdf paper.pdf
@@ -36,7 +36,7 @@
 
 pearl: $(LOG)/HOL-Pearl.gz
 
-$(LOG)/HOL-Pearl.gz: Nominal-General/Nominal*.thy Pearl/ROOT.ML Pearl/document/root.* Pearl/*.thy
+$(LOG)/HOL-Pearl.gz: Pearl/ROOT.ML Pearl/document/root.* Pearl/*.thy
 	@$(USEDIR) -D generated HOL Pearl
 	$(ISABELLE_TOOL) document -o pdf Pearl/generated
 	@cp Pearl/document.pdf pearl.pdf

--- a/Paper/Paper.thy	Sun Apr 04 21:39:28 2010 +0200
+++ b/Paper/Paper.thy	Tue Apr 06 07:36:15 2010 +0200
@@ -1491,7 +1491,7 @@
   "C"}$_{1..m}$, and similar definitions for the free-variable functions @{text
   "fv_ty"}$^\alpha_{1..n}$ and the binding functions @{text
   "bn"}$^\alpha_{1..k}$. However, these definitions are not really useful to the 
-  user, since the are given in terms of the isomorphisms we obtained by 
+  user, since they are given in terms of the isomorphisms we obtained by 
   creating new types in Isabelle/HOL (recall the picture shown in the 
   Introduction).
 
@@ -1562,7 +1562,7 @@
   where the @{text "x\<^isub>i, \<dots>, x\<^isub>j"} are the recursive arguments of @{text "C\<^sup>\<alpha>"}. 
   Next we lift the permutation operations defined in \eqref{ceqvt} for
   the raw term-constructors @{text "C"}. These facts contain, in addition 
-  to the term-constructors, also permutations operations. In order to make the 
+  to the term-constructors, also permutation operations. In order to make the 
   lifting to go through, 
   we have to know that the permutation operations are respectful 
   w.r.t.~alpha-equivalence. This amounts to showing that the 
@@ -1576,7 +1576,7 @@
   \noindent
   for our infrastructure. In a similar fashion we can lift the equations
   characterising the free-variable functions @{text "fn_ty\<AL>\<^isub>j"} and @{text "fv_bn\<AL>\<^isub>k"}, and the 
-  binding functions @{text "bn\<AL>\<^isub>k"}. The necessary respectfulness lemmas for this
+  binding functions @{text "bn\<AL>\<^isub>k"}. The necessary respectfulness lemmas for these
   lifting are the properties:
   %
   \begin{equation}\label{fnresp}