Mercurial Mercurial > repos > isabelle / 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.
src/HOL/Library/Mapping.thy
changeset 55944 7ab8f003fe41
parent 55938 f20d1db5aa3c
child 55945 e96383acecf9 
--- a/src/HOL/Library/Mapping.thy	Thu Mar 06 15:25:21 2014 +0100
+++ b/src/HOL/Library/Mapping.thy	Thu Mar 06 15:29:18 2014 +0100
@@ -43,7 +43,7 @@
 
 lemma map_of_transfer [transfer_rule]:
   assumes [transfer_rule]: "bi_unique R1"
-  shows "(list_all2 (prod_rel R1 R2) ===> R1 ===> rel_option R2) map_of map_of"
+  shows "(list_all2 (rel_prod R1 R2) ===> R1 ===> rel_option R2) map_of map_of"
 unfolding map_of_def by transfer_prover
 
 lemma tabulate_transfer:
isabelle