author | wenzelm |
Sat, 24 Jun 2006 22:25:30 +0200 | |
changeset 19947 | 29b376397cd5 |
parent 19946 | e3ddb0812840 |
child 19948 | 1be283f3f1ba |
src/HOL/Map.thy | file | annotate | diff | comparison | revisions |
--- a/src/HOL/Map.thy Fri Jun 23 13:42:19 2006 +0200 +++ b/src/HOL/Map.thy Sat Jun 24 22:25:30 2006 +0200 @@ -60,7 +60,7 @@ "_MapUpd m (_Maplets xy ms)" == "_MapUpd (_MapUpd m xy) ms" "_MapUpd m (_maplet x y)" == "m(x:=Some y)" "_MapUpd m (_maplets x y)" == "map_upds m x y" - "_Map ms" == "_MapUpd empty ms" + "_Map ms" == "_MapUpd (CONST empty) ms" "_Map (_Maplets ms1 ms2)" <= "_MapUpd (_Map ms1) ms2" "_Maplets ms1 (_Maplets ms2 ms3)" <= "_Maplets (_Maplets ms1 ms2) ms3"