--- a/Paper/Paper.thy	Thu Apr 15 12:07:34 2010 +0200
+++ b/Paper/Paper.thy	Thu Apr 15 12:07:54 2010 +0200
@@ -424,7 +424,7 @@
   permutations.  The sorts of atoms can be used to represent different kinds of
   variables, such as the term-, coercion- and type-variables in Core-Haskell.
   It is assumed that there is an infinite supply of atoms for each
-  sort. However, in the intrest of brevity, we shall restrict ourselves 
+  sort. However, in the interest of brevity, we shall restrict ourselves 
   in what follows to only one sort of atoms.
 
   Permutations are bijective functions from atoms to atoms that are 
@@ -1032,7 +1032,7 @@
 
   As will shortly become clear, we cannot return an atom in a binding function
   that is also bound in the corresponding term-constructor. That means in the
-  example above that the term-constructors @{text PVar} and @{text PTup} must not have a
+  example above that the term-constructors @{text PVar} and @{text PTup} may not have a
   binding clause.  In the version of Nominal Isabelle described here, we also adopted
   the restriction from the Ott-tool that binding functions can only return:
   the empty set or empty list (as in case @{text PNil}), a singleton set or singleton
@@ -2019,7 +2019,7 @@
   definitions to equivariant functions (for such functions it is possible to
   provide more automation).
 
-  There are some restrictions we imposed in this paper, we like to lift in
+  There are some restrictions we imposed in this paper, that we would like to lift in
   future work. One is the exclusion of nested datatype definitions. Nested
   datatype definitions allow one to specify, for instance, the function kinds
   in Core-Haskell as @{text "TFun string (ty list)"} instead of the unfolded