# HG changeset patch
# User Cezary Kaliszyk <kaliszyk@in.tum.de>
# Date 1276404634 -7200
# Node ID fec38b7ceeb303bf3a94cc272d05b17d88bbd53a
# Parent  43e3e8075f3f1b530ee791afb3cb3e5e96c95585
some spelling

diff -r 43e3e8075f3f -r fec38b7ceeb3 Quotient-Paper/Paper.thy
--- 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"}