src/HOL/Map.thy
changeset 19947 29b376397cd5
parent 19656 09be06943252
child 20800 69c82605efcf
equal deleted inserted replaced
19946:e3ddb0812840 19947:29b376397cd5
    58 
    58 
    59 translations
    59 translations
    60   "_MapUpd m (_Maplets xy ms)"  == "_MapUpd (_MapUpd m xy) ms"
    60   "_MapUpd m (_Maplets xy ms)"  == "_MapUpd (_MapUpd m xy) ms"
    61   "_MapUpd m (_maplet  x y)"    == "m(x:=Some y)"
    61   "_MapUpd m (_maplet  x y)"    == "m(x:=Some y)"
    62   "_MapUpd m (_maplets x y)"    == "map_upds m x y"
    62   "_MapUpd m (_maplets x y)"    == "map_upds m x y"
    63   "_Map ms"                     == "_MapUpd empty ms"
    63   "_Map ms"                     == "_MapUpd (CONST empty) ms"
    64   "_Map (_Maplets ms1 ms2)"     <= "_MapUpd (_Map ms1) ms2"
    64   "_Map (_Maplets ms1 ms2)"     <= "_MapUpd (_Map ms1) ms2"
    65   "_Maplets ms1 (_Maplets ms2 ms3)" <= "_Maplets (_Maplets ms1 ms2) ms3"
    65   "_Maplets ms1 (_Maplets ms2 ms3)" <= "_Maplets (_Maplets ms1 ms2) ms3"
    66 
    66 
    67 defs
    67 defs
    68 map_add_def:   "m1++m2 == %x. case m2 x of None => m1 x | Some y => Some y"
    68 map_add_def:   "m1++m2 == %x. case m2 x of None => m1 x | Some y => Some y"