--- a/src/HOL/Library/Mapping.thy Fri Feb 14 07:53:45 2014 +0100
+++ b/src/HOL/Library/Mapping.thy Fri Feb 14 07:53:46 2014 +0100
@@ -65,7 +65,7 @@
lemma map_transfer:
"((A ===> B) ===> (C ===> D) ===> (B ===> option_rel C) ===> A ===> option_rel D)
- (\<lambda>f g m. (Option.map g \<circ> m \<circ> f)) (\<lambda>f g m. (Option.map g \<circ> m \<circ> f))"
+ (\<lambda>f g m. (map_option g \<circ> m \<circ> f)) (\<lambda>f g m. (map_option g \<circ> m \<circ> f))"
by transfer_prover
lemma map_entry_transfer:
@@ -105,13 +105,13 @@
"\<lambda>xs k. if k < length xs then Some (xs ! k) else None" parametric bulkload_transfer .
lift_definition map :: "('c \<Rightarrow> 'a) \<Rightarrow> ('b \<Rightarrow> 'd) \<Rightarrow> ('a, 'b) mapping \<Rightarrow> ('c, 'd) mapping" is
- "\<lambda>f g m. (Option.map g \<circ> m \<circ> f)" parametric map_transfer .
+ "\<lambda>f g m. (map_option g \<circ> m \<circ> f)" parametric map_transfer .
subsection {* Functorial structure *}
enriched_type map: map
- by (transfer, auto simp add: fun_eq_iff Option.map.compositionality Option.map.id)+
+ by (transfer, auto simp add: fun_eq_iff option.map_comp option.map_id)+
subsection {* Derived operations *}
@@ -367,5 +367,3 @@
replace default map_entry map_default tabulate bulkload map of_alist
end
-
-