# HG changeset patch
# User nipkow
# Date 1453049793 -3600
# Node ID 66fb3d1767f2a7d4f6571d9d33ff16f426e214cc
# Parent  799a5306e2ed4302fb3ac1c4761173c4118554eb
renamed map_of to lookup

diff -r 799a5306e2ed -r 66fb3d1767f2 src/HOL/Data_Structures/Map_by_Ordered.thy
--- a/src/HOL/Data_Structures/Map_by_Ordered.thy	Sun Jan 17 00:14:45 2016 +0100
+++ b/src/HOL/Data_Structures/Map_by_Ordered.thy	Sun Jan 17 17:56:33 2016 +0100
@@ -10,11 +10,11 @@
 fixes empty :: "'m"
 fixes update :: "'a \<Rightarrow> 'b \<Rightarrow> 'm \<Rightarrow> 'm"
 fixes delete :: "'a \<Rightarrow> 'm \<Rightarrow> 'm"
-fixes map_of :: "'m \<Rightarrow> 'a \<Rightarrow> 'b option"
+fixes lookup :: "'m \<Rightarrow> 'a \<Rightarrow> 'b option"
 fixes invar :: "'m \<Rightarrow> bool"
-assumes map_empty: "map_of empty = (\<lambda>_. None)"
-and map_update: "invar m \<Longrightarrow> map_of(update a b m) = (map_of m)(a := Some b)"
-and map_delete: "invar m \<Longrightarrow> map_of(delete a m) = (map_of m)(a := None)"
+assumes map_empty: "lookup empty = (\<lambda>_. None)"
+and map_update: "invar m \<Longrightarrow> lookup(update a b m) = (lookup m)(a := Some b)"
+and map_delete: "invar m \<Longrightarrow> lookup(delete a m) = (lookup m)(a := None)"
 and invar_empty: "invar empty"
 and invar_update: "invar m \<Longrightarrow> invar(update a b m)"
 and invar_delete: "invar m \<Longrightarrow> invar(delete a m)"