src/HOL/Map.thy
changeset 61069 aefe89038dd2
parent 61032 b57df8eecad6
child 61799 4cf66f21b764
     1.1 --- a/src/HOL/Map.thy	Mon Aug 31 20:56:24 2015 +0200
     1.2 +++ b/src/HOL/Map.thy	Mon Aug 31 21:01:21 2015 +0200
     1.3 @@ -11,21 +11,15 @@
     1.4  imports List
     1.5  begin
     1.6  
     1.7 -type_synonym ('a, 'b) "map" = "'a \<Rightarrow> 'b option" (infixr "~=>" 0)
     1.8 -
     1.9 -type_notation (xsymbols)
    1.10 -  "map" (infixr "\<rightharpoonup>" 0)
    1.11 +type_synonym ('a, 'b) "map" = "'a \<Rightarrow> 'b option" (infixr "\<rightharpoonup>" 0)
    1.12  
    1.13  abbreviation
    1.14    empty :: "'a \<rightharpoonup> 'b" where
    1.15    "empty \<equiv> \<lambda>x. None"
    1.16  
    1.17  definition
    1.18 -  map_comp :: "('b \<rightharpoonup> 'c) \<Rightarrow> ('a \<rightharpoonup> 'b) \<Rightarrow> ('a \<rightharpoonup> 'c)"  (infixl "o'_m" 55) where
    1.19 -  "f o_m g = (\<lambda>k. case g k of None \<Rightarrow> None | Some v \<Rightarrow> f v)"
    1.20 -
    1.21 -notation (xsymbols)
    1.22 -  map_comp  (infixl "\<circ>\<^sub>m" 55)
    1.23 +  map_comp :: "('b \<rightharpoonup> 'c) \<Rightarrow> ('a \<rightharpoonup> 'b) \<Rightarrow> ('a \<rightharpoonup> 'c)"  (infixl "\<circ>\<^sub>m" 55) where
    1.24 +  "f \<circ>\<^sub>m g = (\<lambda>k. case g k of None \<Rightarrow> None | Some v \<Rightarrow> f v)"
    1.25  
    1.26  definition
    1.27    map_add :: "('a \<rightharpoonup> 'b) \<Rightarrow> ('a \<rightharpoonup> 'b) \<Rightarrow> ('a \<rightharpoonup> 'b)"  (infixl "++" 100) where