Mercurial Mercurial > hg > nominal2 / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Quot/QuotScript.thy
changeset 674 bb276771d85c
parent 656 c86a47d4966e
child 696 fd718dde1d61 
--- a/Quot/QuotScript.thy	Wed Dec 09 22:05:11 2009 +0100
+++ b/Quot/QuotScript.thy	Wed Dec 09 22:43:11 2009 +0100
@@ -510,7 +510,7 @@
 lemma rep_abs_rsp_left:
   assumes q: "Quotient R Abs Rep"
   and     a: "R x1 x2"
-  shows "R x1 (Rep (Abs x2))"
+  shows "R (Rep (Abs x1)) x2"
 using q a by (metis Quotient_rel[OF q] Quotient_abs_rep[OF q] Quotient_rep_reflp[OF q])
nominal2