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.
Quotients.thy
changeset 3 672e14609e6e
parent 0 ebe0ea8fe247
child 538 bce41bea3de2 
--- a/Quotients.thy	Thu Aug 20 10:31:44 2009 +0200
+++ b/Quotients.thy	Thu Aug 20 14:44:29 2009 +0200
@@ -138,7 +138,7 @@
 lemma QUOTIENT_PROD:
   assumes a: "QUOTIENT E1 Abs1 Rep1"
   and     b: "QUOTIENT E2 Abs2 Rep2"
-  shows "QUOTIENT (PROD_REL E1 e2) (prod_map Abs1 Abs2) (prod_map Rep1 rep2)"
+  shows "QUOTIENT (PROD_REL E1 E2) (prod_map Abs1 Abs2) (prod_map Rep1 Rep2)"
 using a b unfolding QUOTIENT_def
 oops
nominal2