src/HOL/Library/Mapping.thy
changeset 55938 f20d1db5aa3c
parent 55525 70b7e91fa1f9
child 55944 7ab8f003fe41
     1.1 --- a/src/HOL/Library/Mapping.thy	Thu Mar 06 14:25:55 2014 +0100
     1.2 +++ b/src/HOL/Library/Mapping.thy	Thu Mar 06 14:57:14 2014 +0100
     1.3 @@ -37,7 +37,7 @@
     1.4  
     1.5  lemma dom_transfer:
     1.6    assumes [transfer_rule]: "bi_total A"
     1.7 -  shows "((A ===> rel_option B) ===> set_rel A) dom dom" 
     1.8 +  shows "((A ===> rel_option B) ===> rel_set A) dom dom" 
     1.9  unfolding dom_def[abs_def] equal_None_def[symmetric] 
    1.10  by transfer_prover
    1.11