# 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)"  \<rightleftharpoons> "_MapUpd (_MapUpd m xy) ms"
   "_MapUpd m (_maplet  x y)"    \<rightleftharpoons> "m(x := CONST Some y)"
   "_Map ms"                     \<rightleftharpoons> "_MapUpd (CONST empty) ms"
+  "_Map ms"                     \<leftharpoondown> "_MapUpd (\<lambda>x. CONST None) ms" \<comment>\<open>both are needed\<close>
   "_Map (_Maplets ms1 ms2)"     \<leftharpoondown> "_MapUpd (_Map ms1) ms2"
   "_Maplets ms1 (_Maplets ms2 ms3)" \<leftharpoondown> "_Maplets (_Maplets ms1 ms2) ms3"