--- a/Quotient-Paper/Paper.thy	Thu Aug 26 02:08:00 2010 +0800
+++ b/Quotient-Paper/Paper.thy	Thu Aug 26 14:55:15 2010 +0900
@@ -1049,7 +1049,7 @@
   We defined the theorem @{text "inj_thm"} in such a way that
   establishing the equivalence @{text "inj_thm \<longleftrightarrow> quot_thm"} can be
   achieved by rewriting @{text "inj_thm"} with the preservation theorems and quotient
-  definitions. Next the definitions of all lifted constants
+  definitions. First the definitions of all lifted constants
   are used to fold the @{term Rep} with the raw constants. Next for
   all abstractions and quantifiers the lambda and
   quantifier preservation theorems are used to replace the