--- a/Paper/Paper.thy	Sat May 29 00:16:39 2010 +0200
+++ b/Paper/Paper.thy	Tue Jun 01 15:45:43 2010 +0200
@@ -937,8 +937,8 @@
 
   \noindent
   Similarly for the other binding modes. Interestingly, in case of \isacommand{bind\_set}
-  and \isacommand{bind\_res} the binding clauses will make a difference to the semantics
-  of the specification (the corresponding alpha-equivalence will differ). We will 
+  and \isacommand{bind\_res} the binding clauses above will make a difference to the semantics
+  of the specifications (the corresponding alpha-equivalence will differ). We will 
   show this later with an example.
   
   There are some restrictions we need to impose on binding clasues: First, a
@@ -1058,7 +1058,6 @@
   "bn(as)"} in the term @{text t}, but with @{text "Let_rec"} we also want to bind the atoms
   inside the assignment. This difference has consequences for the free-variable 
   function and alpha-equivalence relation, which we are going to define below.
-  
   For this definition, we have to impose some restrictions on deep binders. First,
   we cannot have more than one binding function for one binder. So we exclude: