src/HOL/Map.thy
changeset 25490 e8ab1c42c14f
parent 25483 65de74f62874
child 25670 497474b69c86
equal deleted inserted replaced
25489:5b0625f6e324 25490:e8ab1c42c14f
    10 
    10 
    11 theory Map
    11 theory Map
    12 imports List
    12 imports List
    13 begin
    13 begin
    14 
    14 
    15 types ('a,'b) map = "'a => 'b option"  (infixr "~=>" 0)
    15 types ('a,'b) "~=>" = "'a => 'b option"  (infixr 0)
    16 translations (type) "a ~=> b " <= (type) "a => b option"
    16 translations (type) "a ~=> b " <= (type) "a => b option"
    17 
    17 
    18 syntax (xsymbols)
    18 syntax (xsymbols)
    19   map :: "type \<Rightarrow> type \<Rightarrow> type"  (infixr "\<rightharpoonup>" 0)
    19   "~=>" :: "[type, type] => type"  (infixr "\<rightharpoonup>" 0)
    20 
    20 
    21 abbreviation
    21 abbreviation
    22   empty :: "'a ~=> 'b" where
    22   empty :: "'a ~=> 'b" where
    23   "empty == %x. None"
    23   "empty == %x. None"
    24 
    24