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