src/HOL/Library/Mapping.thy
changeset 55944 7ab8f003fe41
parent 55938 f20d1db5aa3c
child 55945 e96383acecf9
     1.1 --- a/src/HOL/Library/Mapping.thy	Thu Mar 06 15:25:21 2014 +0100
     1.2 +++ b/src/HOL/Library/Mapping.thy	Thu Mar 06 15:29:18 2014 +0100
     1.3 @@ -43,7 +43,7 @@
     1.4  
     1.5  lemma map_of_transfer [transfer_rule]:
     1.6    assumes [transfer_rule]: "bi_unique R1"
     1.7 -  shows "(list_all2 (prod_rel R1 R2) ===> R1 ===> rel_option R2) map_of map_of"
     1.8 +  shows "(list_all2 (rel_prod R1 R2) ===> R1 ===> rel_option R2) map_of map_of"
     1.9  unfolding map_of_def by transfer_prover
    1.10  
    1.11  lemma tabulate_transfer: