# HG changeset patch
# User Cezary Kaliszyk <kaliszyk@in.tum.de>
# Date 1282802115 -32400
# Node ID 319f469b8b67f3838d094bc8decba7da106f05dd
# Parent  3885dc2669f9052800210f700a76d2b04720383f
minor

diff -r 3885dc2669f9 -r 319f469b8b67 Quotient-Paper/Paper.thy
--- 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