--- 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"
--- 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"
--- 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