src/HOL/Map.thy
changeset 80934 8e72f55295fd
parent 80932 261cd8722677
child 81125 ec121999a9cb
--- a/src/HOL/Map.thy	Mon Sep 23 15:01:10 2024 +0200
+++ b/src/HOL/Map.thy	Mon Sep 23 21:09:23 2024 +0200
@@ -61,7 +61,7 @@
   ""         :: "maplet \<Rightarrow> updbind"              (\<open>_\<close>)
   ""         :: "maplet \<Rightarrow> maplets"             (\<open>_\<close>)
   "_Maplets" :: "[maplet, maplets] \<Rightarrow> maplets" (\<open>_,/ _\<close>)
-  "_Map"     :: "maplets \<Rightarrow> 'a \<rightharpoonup> 'b"           (\<open>(1[_])\<close>)
+  "_Map"     :: "maplets \<Rightarrow> 'a \<rightharpoonup> 'b"           (\<open>(\<open>indent=1 notation=\<open>mixfix maplets\<close>\<close>[_])\<close>)
 (* Syntax forbids \<open>[\<dots>, x := y, \<dots>]\<close> by introducing \<open>maplets\<close> in addition to \<open>updbinds\<close> *)
 
 syntax (ASCII)