--- a/src/HOL/Library/Mapping.thy Tue Jun 21 17:35:45 2016 +0200
+++ b/src/HOL/Library/Mapping.thy Wed Jun 22 10:09:20 2016 +0200
@@ -14,11 +14,9 @@
"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
@@ -219,11 +217,9 @@
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"