Mercurial Mercurial > hg > nominal2 / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
merged
authorChristian Urban <urbanc@in.tum.de>
Fri, 27 Aug 2010 02:08:36 +0800
changeset 2439 cc6e281d8f72
parent 2438 abafea9b39bb (current diff)
parent 2437 319f469b8b67 (diff)
child 2440 0a36825b16c1
merged
--- 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
nominal2