src/HOL/Library/Mapping.thy

 
 lemma map_of_foldr: \<comment> \<open>FIXME move\<close>
   "map_of xs = foldr (\<lambda>(k, v) m. m(k \<mapsto> v)) xs Map.empty"
   using map_add_map_of_foldr [of Map.empty] by auto
 
-context
+context includes lifting_syntax
 begin
-
-interpretation lifting_syntax .
 
 lemma empty_parametric:
   "(A ===> rel_option B) Map.empty Map.empty"
   by transfer_prover
 

 instance
   by standard (unfold equal_mapping_def, transfer, auto)
 
 end
 
-context
+context includes lifting_syntax
 begin
-
-interpretation lifting_syntax .
 
 lemma [transfer_rule]:
   assumes [transfer_rule]: "bi_total A"
   assumes [transfer_rule]: "bi_unique B"
   shows "(pcr_mapping A B ===> pcr_mapping A B ===> op=) HOL.eq HOL.equal"