--- a/Quotient-Paper/Paper.thy	Mon Jun 14 12:30:08 2010 +0200
+++ b/Quotient-Paper/Paper.thy	Mon Jun 14 14:28:12 2010 +0200
@@ -113,7 +113,7 @@
   from the raw type @{typ "nat \<times> nat"} to the quotient type @{typ int}
   (similarly for finite sets and $\alpha$-equated lambda-terms). This lifting
   usually requires a \emph{lot} of tedious reasoning effort \cite{Paulson06}.  
-  It is feasible to to this work manually, if one has only a few quotient
+  It is feasible to do this work manually, if one has only a few quotient
   constructions at hand. But if they have to be done over and over again, as in 
   Nominal Isabelle, then manual reasoning is not an option.
 
@@ -158,7 +158,7 @@
   and @{text Rep}.\footnote{Actually slightly more basic functions are given;
   the functions @{text Abs} and @{text Rep} need to be derived from them. We
   will show the details later. } These functions relate elements in the
-  existing type to ones in the new type and vice versa; they can be uniquely
+  existing type to elements in the new type and vice versa; they can be uniquely
   identified by their type. For example for the integer quotient construction
   the types of @{text Abs} and @{text Rep} are
 
@@ -236,21 +236,22 @@
   of \emph{aggregate equivalence relation}, \emph{respectfulness} and \emph{preservation}
   from Homeier \cite{Homeier05}.
 
-  We are also able to address the criticism by Paulson \cite{Paulson06} cited
+  In addition we are able to address the criticism by Paulson \cite{Paulson06} cited
   at the beginning of this section about having to collect theorems that are
   lifted from the raw level to the quotient level into one giant list. Our
   quotient package is the first one that is modular so that it allows to lift
-  single theorems separately. This has the advantage for the user to develop a
-  formal theory interactively an a natural progression. A pleasing result of
-  the modularity is also that we are able to clearly specify what needs to be
+  single theorems separately. This has the advantage for the user of being able to develop a
+  formal theory interactively as a natural progression. A pleasing side-result of
+  the modularity is that we are able to clearly specify what needs to be
   done in the lifting process (this was only hinted at in \cite{Homeier05} and
   implemented as a ``rough recipe'' in ML-code).
 
 
   The paper is organised as follows: Section \ref{sec:prelims} presents briefly
   some necessary preliminaries; Section \ref{sec:type} describes the definitions 
-  of quotient types and shows how definition of constants can be made over 
-  quotient types. \ldots
+  of quotient types and shows how definitions of constants can be made over 
+  quotient types. Section \ref{sec:resp} introduces the notions of respectfullness
+  and preservation.\ldots
 *}
 
 
@@ -376,12 +377,13 @@
   respectively.  Given that @{text "R"} is an equivalence relation, the
   following property
 
-
-  @{text [display, indent=10] "Quotient R Abs_\<kappa>\<^isub>q Rep_\<kappa>\<^isub>q"}
+  \begin{property}
+  @{text "Quotient R Abs_\<kappa>\<^isub>q Rep_\<kappa>\<^isub>q"}
+  \end{property}
 
   \noindent
-  holds (for the proof see \cite{Homeier05}) for every quotient type defined
-  as above.
+  holds  for every quotient type defined
+  as above (for the proof see \cite{Homeier05}).
 
   The next step in a quotient construction is to introduce definitions of new constants
   involving the quotient type. These definitions need to be given in terms of concepts
@@ -415,7 +417,7 @@
   quotient types involved. The data we rely on is the given quotient type
   @{text "\<tau>"} and the raw type @{text "\<sigma>"}.  They allow us to define \emph{aggregate
   abstraction} and \emph{representation functions} using the functions @{text "ABS (\<sigma>,
-  \<tau>)"} and @{text "REP (\<sigma>, \<tau>)"} whose clauses we given below. The idea behind
+  \<tau>)"} and @{text "REP (\<sigma>, \<tau>)"} whose clauses we give below. The idea behind
   these two functions is to recursively descend into the raw types @{text \<sigma>} and 
   quotient types @{text \<tau>}, and generate the appropriate
   @{text "Abs"} and @{text "Rep"} in places where the types differ. Therefore
@@ -423,6 +425,7 @@
   are as follows:
 
   \begin{center}
+  \hfill
   \begin{tabular}{rcl}
   \multicolumn{3}{@ {\hspace{-4mm}}l}{equal types:}\\ 
   @{text "ABS (\<sigma>, \<sigma>)"} & $\dn$ & @{text "id :: \<sigma> \<Rightarrow> \<sigma>"}\\
@@ -460,7 +463,7 @@
   \end{center}
   %
   \noindent
-  In this definition we abuse the fact that we can interpret type-variables @{text \<alpha>} as 
+  In this definition we rely on the fact that we can interpret type-variables @{text \<alpha>} as 
   term variables @{text a}. In the last clause we build an abstraction over all
   term-variables inside map-function generated by the auxiliary function 
   @{text "MAP'"}.
@@ -498,10 +501,8 @@
   \noindent
   Note that by using the operator @{text "\<singlearr>"} and special clauses
   for function types in \eqref{ABSREP}, we do not have to 
-  distinguish between arguments and results: the representation and abstraction
-  functions are just inverses of each other, which we can combine using 
-  @{text "\<singlearr>"} to deal uniformly with arguments of functions and 
-  their result. Consequently, all definitions in the quotient package 
+  distinguish between arguments and results, but can deal with them uniformly.
+  Consequently, all definitions in the quotient package 
   are of the general form
 
   @{text [display, indent=10] "c \<equiv> ABS (\<sigma>, \<tau>) t"}
@@ -510,7 +511,7 @@
   where @{text \<sigma>} is the type of the definiens @{text "t"} and @{text "\<tau>"} the
   type of the defined quotient constant @{text "c"}. This data can be easily
   generated from the declaration given by the user.
-  To increase the confidence of making correct definitions, we can prove 
+  To increase the confidence in this way of making definitions, we can prove 
   that the terms involved are all typable.
 
   \begin{lemma}
@@ -544,7 +545,7 @@
   functions used, for example, in Homeier's quotient package.
 *}
 
-section {* Respectfulness and Preservation *}
+section {* Respectfulness and Preservation \label{sec:resp} *}
 
 text {*
   The main point of the quotient package is to automatically ``lift'' theorems
@@ -556,8 +557,8 @@
   raw lambda-terms as follows
 
   \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%
-  @{text "bn (x) \<equiv> \<emptyset>"}\hspace{5mm}
-  @{text "bn (t\<^isub>1 t\<^isub>2) \<equiv> bn (t\<^isub>1) \<union> bn (t\<^isub>2)"}\hspace{5mm}
+  @{text "bn (x) \<equiv> \<emptyset>"}\hspace{4mm}
+  @{text "bn (t\<^isub>1 t\<^isub>2) \<equiv> bn (t\<^isub>1) \<union> bn (t\<^isub>2)"}\hspace{4mm}
   @{text "bn (\<lambda>x. t) \<equiv> {x} \<union> bn (t)"}
   \end{isabelle}