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/QuotSum.thy
changeset 779 3b21b24a5fb6
parent 698 ed44eaaea63e
child 829 42b90994ac77 
--- a/Quot/QuotSum.thy	Tue Dec 22 22:10:48 2009 +0100
+++ b/Quot/QuotSum.thy	Wed Dec 23 10:31:54 2009 +0100
@@ -16,7 +16,8 @@
   "sum_map f1 f2 (Inl a) = Inl (f1 a)"
 | "sum_map f1 f2 (Inr a) = Inr (f2 a)"
 
-declare [[map * = (sum_map, sum_rel)]]
+declare [[map "+" = (sum_map, sum_rel)]]
+
 
 lemma sum_equivp[quot_equiv]:
   assumes a: "equivp R1"
nominal2