src/HOL/Map.thy
changeset 35115 446c5063e4fd
parent 34979 8cb6e7a42e9c
child 35159 df38e92af926
     1.1 --- a/src/HOL/Map.thy	Thu Feb 11 22:55:16 2010 +0100
     1.2 +++ b/src/HOL/Map.thy	Thu Feb 11 23:00:22 2010 +0100
     1.3 @@ -68,7 +68,7 @@
     1.4  
     1.5  translations
     1.6    "_MapUpd m (_Maplets xy ms)"  == "_MapUpd (_MapUpd m xy) ms"
     1.7 -  "_MapUpd m (_maplet  x y)"    == "m(x:=Some y)"
     1.8 +  "_MapUpd m (_maplet  x y)"    == "m(x := CONST Some y)"
     1.9    "_Map ms"                     == "_MapUpd (CONST empty) ms"
    1.10    "_Map (_Maplets ms1 ms2)"     <= "_MapUpd (_Map ms1) ms2"
    1.11    "_Maplets ms1 (_Maplets ms2 ms3)" <= "_Maplets (_Maplets ms1 ms2) ms3"