--- a/Quotient-Paper/Paper.thy	Fri Aug 27 02:03:52 2010 +0800
+++ b/Quotient-Paper/Paper.thy	Fri Aug 27 02:08:36 2010 +0800
@@ -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