# HG changeset patch
# User wenzelm
# Date 1727694042 -7200
# Node ID 83596aea48cb59a88a6903e6f7ccd4264862c7bf
# Parent  bc5eb7841b74acde457cf37de38e021c820e7d4e
less markup: prefer "notatation" over "entity";

diff -r bc5eb7841b74 -r 83596aea48cb src/HOL/Fun.thy
--- a/src/HOL/Fun.thy	Mon Sep 30 12:59:50 2024 +0200
+++ b/src/HOL/Fun.thy	Mon Sep 30 13:00:42 2024 +0200
@@ -844,10 +844,10 @@
   "_updbind" :: "'a \<Rightarrow> 'a \<Rightarrow> updbind"             (\<open>(\<open>indent=2 notation=\<open>mixfix update\<close>\<close>_ :=/ _)\<close>)
   ""         :: "updbind \<Rightarrow> updbinds"             (\<open>_\<close>)
   "_updbinds":: "updbind \<Rightarrow> updbinds \<Rightarrow> updbinds" (\<open>_,/ _\<close>)
-  "_Update"  :: "'a \<Rightarrow> updbinds \<Rightarrow> 'a"            (\<open>_/'((\<open>indent=2 notation=\<open>mixfix updates\<close>\<close>_)')\<close> [1000, 0] 900)
+  "_Update"  :: "'a \<Rightarrow> updbinds \<Rightarrow> 'a"            (\<open>_/'((2_)')\<close> [1000, 0] 900)
 
 syntax_consts
-  "_updbind" "_updbinds" "_Update" \<rightleftharpoons> fun_upd
+  fun_upd
 
 translations
   "_Update f (_updbinds b bs)" \<rightleftharpoons> "_Update (_Update f b) bs"
diff -r bc5eb7841b74 -r 83596aea48cb src/HOL/List.thy
--- a/src/HOL/List.thy	Mon Sep 30 12:59:50 2024 +0200
+++ b/src/HOL/List.thy	Mon Sep 30 13:00:42 2024 +0200
@@ -141,7 +141,7 @@
   "_LUpdate" :: "['a, lupdbinds] => 'a"    (\<open>_/[(_)]\<close> [1000,0] 900)
 
 syntax_consts
-  "_lupdbind" "_lupdbinds" "_LUpdate" == list_update
+  list_update
 
 translations
   "_LUpdate xs (_lupdbinds b bs)" == "_LUpdate (_LUpdate xs b) bs"
diff -r bc5eb7841b74 -r 83596aea48cb src/HOL/Product_Type.thy
--- a/src/HOL/Product_Type.thy	Mon Sep 30 12:59:50 2024 +0200
+++ b/src/HOL/Product_Type.thy	Mon Sep 30 13:00:42 2024 +0200
@@ -294,7 +294,7 @@
   "_patterns"   :: "pttrn \<Rightarrow> patterns \<Rightarrow> patterns"      (\<open>_,/ _\<close>)
   "_unit"       :: pttrn                                (\<open>'(')\<close>)
 syntax_consts
-  "_tuple" "_tuple_arg" "_tuple_args" \<rightleftharpoons> Pair and
+  Pair and
   "_pattern" "_patterns" \<rightleftharpoons> case_prod and
   "_unit" \<rightleftharpoons> case_unit
 translations