--- a/Quotient-Paper/Paper.thy	Sun Jun 13 06:45:20 2010 +0200
+++ b/Quotient-Paper/Paper.thy	Sun Jun 13 06:50:34 2010 +0200
@@ -352,7 +352,7 @@
 
   Apart from the last 2 points the definition is same as the one implemented in
   in Homeier's HOL package. Adding composition in last two cases is necessary
-  for compositional quotients. We ilustrate the different behaviour of the
+  for compositional quotients. We illustrate the different behaviour of the
   definition by showing the derived definition of @{term fconcat}:
 
   @{thm fconcat_def[no_vars]}
@@ -544,13 +544,13 @@
   \item @{text "REG (c\<^isub>1, c\<^isub>2) = c\<^isub>1"}
   \end{itemize}
 
-  In the above definition we ommited the cases for existential quantifiers
+  In the above definition we omitted the cases for existential quantifiers
   and unique existential quantifiers, as they are very similar to the cases
   for the universal quantifier.
 
   Next we define the function @{text INJ} which takes the statement of
   the regularized theorems and the statement of the lifted theorem both as
-  terms and returns the statment of the injected theorem:
+  terms and returns the statement of the injected theorem:
 
   \begin{itemize}
   \item @{text "INJ ((\<lambda>x. t) : \<sigma>, (\<lambda>x. s) : \<sigma>) = \<lambda>x. (INJ (t, s)"}
@@ -566,7 +566,7 @@
   \end{itemize}
 
   For existential quantifiers and unique existential quantifiers it is
-  defined similarily to the universal one.
+  defined similarly to the universal one.
 
 *}
 
@@ -610,10 +610,10 @@
 text {*
 
   Isabelle provides a set of \emph{mono} rules, that are used to split implications
-  of similar statements into simpler implication subgoals. These are enchanced
+  of similar statements into simpler implication subgoals. These are enhanced
   with special quotient theorem in the regularization goal. Below we only show
   the versions for the universal quantifier. For the existential quantifier
-  and abstraction they are analoguous with some symmetry.
+  and abstraction they are analogous with some symmetry.
 
   First, bounded universal quantifiers can be removed on the right:
 
@@ -727,7 +727,7 @@
   Can be proved automatically by the system just by unfolding the definition
   of @{term "op \<Longrightarrow>"}.
 
-  Now the user can either prove a lifted lemma explicitely:
+  Now the user can either prove a lifted lemma explicitly:
 
   @{text "lemma 0 + i = i by lifting plus_zero_raw"}