diff -r 229660b9f2fc -r 0f3c497fb3b0 Quotient-Paper/Paper.thy
--- a/Quotient-Paper/Paper.thy	Thu Jun 17 07:34:29 2010 +0200
+++ b/Quotient-Paper/Paper.thy	Thu Jun 17 07:37:26 2010 +0200
@@ -247,7 +247,8 @@
   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
-%%% FIXME: First-order ones exist, HOL-Light one lifts theorems separately.
+%%% FIXME: First-order ones exist, for example in HOL-Light the lift_theorem function
+%%% takes all the prerequisites and one single theorem to lift.
   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 is involved
@@ -398,7 +399,7 @@
   would not be true in general. However, we can prove specific and useful 
   instances of the quotient theorem. We will 
   show an example in Section \ref{sec:resp}.
-%%% FIXME the example is gone from the paper?
+%%% FIXME the example is gone from the paper? Maybe we can just put it here?
 
 *}
 
@@ -925,7 +926,7 @@
   In the first proof step, establishing @{text "raw_thm \<longrightarrow> reg_thm"}, we always 
   start with an implication. Isabelle provides \emph{mono} rules that can split up 
   the implications into simpler implication subgoals. This succeeds for every
-  monotone connective, except in places wher the function @{text REG} inserted,
+  monotone connective, except in places where the function @{text REG} inserted,
   for example, a quantifier by a bounded quantifier. In this case we have 
   rules of the form
 
@@ -1004,7 +1005,7 @@
 
   In this section we will show, a complete interaction with the quotient package
   for defining the type of integers by quotienting pairs of natural numbers and
-  lifting theorems to integers. Oeur quotient package is fully compatible with
+  lifting theorems to integers. Our quotient package is fully compatible with
   Isabelle type classes, but for clarity we will not use them in this example.
   In a larger formalization of integers using the type class mechanism would
   provide many algebraic properties ``for free''.
@@ -1065,7 +1066,7 @@
   \end{isabelle}
 
   \noindent
-  This can be dischaged automatically by Isabelle when telling it to unfold the definition
+  This can be discharged automatically by Isabelle when telling it to unfold the definition
   of @{text "\<doublearr>"}.
   After this, the user can prove the lifted lemma explicitly:
 
@@ -1114,13 +1115,14 @@
   defines quotient types for Isabelle/HOL. But he did not include theorem lifting.
   Harrison's quotient package~\cite{harrison-thesis} is the first one that is
   able to automatically lift theorems, however only first-order theorems (that is theorems
-  where abstractions, quantifiers and variables do not involve the quotient type). 
+  where abstractions, quantifiers and variables do not involve functions that
+  include the quotient type). 
   There is also some work on quotient types in
   non-HOL based systems and logical frameworks, including theory interpretations
   in PVS~\cite{PVS:Interpretations}, new types in MetaPRL~\cite{Nogin02}, 
   and setoids in Coq \cite{ChicliPS02}.
   Paulson showed a construction of quotients that does not require the
-  Hilbert Choice operator, but also only first-order theorems to be lifted~\cite{Paulson06}.
+  Hilbert Choice operator, but also only first-order theorems can be lifted~\cite{Paulson06}.
   The most related work to our package is the package for HOL4 by Homeier~\cite{Homeier05}.
   He introduced most of the abstract notions about quotients and also deals with the
   lifting of higher-order theorems. However, he cannot deal with quotient compositions (needed