# HG changeset patch
# User haftmann
# Date 1387812583 -3600
# Node ID a435932a9f12c2a8c4a54541d388092f6bf96265
# Parent  7137303f9f88029b295fdac3b36ea3ed056aac42
prefer Y_of_X over X_to_Y;
prefer alist over assoc_list;
prefer explicit prefix

diff -r 7137303f9f88 -r a435932a9f12 src/HOL/Library/Mapping.thy
--- a/src/HOL/Library/Mapping.thy	Mon Dec 23 16:59:56 2013 +0100
+++ b/src/HOL/Library/Mapping.thy	Mon Dec 23 16:29:43 2013 +0100
@@ -142,11 +142,11 @@
 definition map_default :: "'a \<Rightarrow> 'b \<Rightarrow> ('b \<Rightarrow> 'b) \<Rightarrow> ('a, 'b) mapping \<Rightarrow> ('a, 'b) mapping" where
   "map_default k v f m = map_entry k f (default k v m)" 
 
-lift_definition assoc_list_to_mapping :: "('k \<times> 'v) list \<Rightarrow> ('k, 'v) mapping"
+lift_definition of_alist :: "('k \<times> 'v) list \<Rightarrow> ('k, 'v) mapping"
 is map_of parametric map_of_transfer .
 
-lemma assoc_list_to_mapping_code [code]:
-  "assoc_list_to_mapping xs = foldr (\<lambda>(k, v) m. update k v m) xs empty"
+lemma of_alist_code [code]:
+  "of_alist xs = foldr (\<lambda>(k, v) m. update k v m) xs empty"
 by transfer(simp add: map_add_map_of_foldr[symmetric])
 
 instantiation mapping :: (type, type) equal
@@ -364,7 +364,7 @@
 code_datatype empty update
 
 hide_const (open) empty is_empty rep lookup update delete ordered_keys keys size
-  replace default map_entry map_default tabulate bulkload map
+  replace default map_entry map_default tabulate bulkload map of_alist
 
 end