# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1282846116 -28800
# Node ID cc6e281d8f72afb9c68658d3d216ff25785abe8c
# Parent  abafea9b39bbe4c22fa9314d7e92cc2aecd2573b# Parent  319f469b8b67f3838d094bc8decba7da106f05dd
merged

diff -r abafea9b39bb -r cc6e281d8f72 Quotient-Paper/Paper.thy
--- 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