# HG changeset patch # User nipkow # Date 1677240890 -3600 # Node ID b34435f2a2bf83bd3ed14410bf7c38d75da476bd # Parent ef03267af5a75a5851bbe73eaf0d6e9cbaf19bfc brought back [...] maplet syntax diff -r ef03267af5a7 -r b34435f2a2bf src/HOL/Map.thy --- a/src/HOL/Map.thy Fri Feb 24 10:59:59 2023 +0000 +++ b/src/HOL/Map.thy Fri Feb 24 13:14:50 2023 +0100 @@ -67,6 +67,7 @@ "_MapUpd m (_Maplets xy ms)" \ "_MapUpd (_MapUpd m xy) ms" "_MapUpd m (_maplet x y)" \ "m(x := CONST Some y)" "_Map ms" \ "_MapUpd (CONST empty) ms" + "_Map ms" \ "_MapUpd (\x. CONST None) ms" \\both are needed\ "_Map (_Maplets ms1 ms2)" \ "_MapUpd (_Map ms1) ms2" "_Maplets ms1 (_Maplets ms2 ms3)" \ "_Maplets (_Maplets ms1 ms2) ms3"