src/HOL/Library/Dlist.thy
changeset 67399 eab6ce8368fa
parent 63375 59803048b0e8
child 69593 3dda49e08b9d
     1.1 --- a/src/HOL/Library/Dlist.thy	Wed Jan 10 15:21:49 2018 +0100
     1.2 +++ b/src/HOL/Library/Dlist.thy	Wed Jan 10 15:25:09 2018 +0100
     1.3 @@ -316,7 +316,7 @@
     1.4  qualified lift_definition set :: "'a dlist \<Rightarrow> 'a set" is List.set .
     1.5  
     1.6  qualified lemma map_transfer [transfer_rule]:
     1.7 -  "(rel_fun op = (rel_fun (pcr_dlist op =) (pcr_dlist op =))) (\<lambda>f x. remdups (List.map f x)) Dlist.map"
     1.8 +  "(rel_fun (=) (rel_fun (pcr_dlist (=)) (pcr_dlist (=)))) (\<lambda>f x. remdups (List.map f x)) Dlist.map"
     1.9  by(simp add: rel_fun_def dlist.pcr_cr_eq cr_dlist_def Dlist.map_def remdups_remdups)
    1.10  
    1.11  bnf "'a dlist"