# HG changeset patch
# User wenzelm
# Date 1728382235 -7200
# Node ID ec121999a9cbe3265571352d916f358f86023416
# Parent  6ce0c8d59f5acfaaf9f11117dc3b07bd95a8de95
more inner-syntax markup;
more syntax bundles for use with "unbundle no foobar_syntax";

diff -r 6ce0c8d59f5a -r ec121999a9cb NEWS
--- a/NEWS	Sun Oct 06 22:56:07 2024 +0200
+++ b/NEWS	Tue Oct 08 12:10:35 2024 +0200
@@ -69,6 +69,9 @@
   unbundle no rtrancl_syntax
   unbundle no trancl_syntax
   unbundle no reflcl_syntax
+  unbundle no abs_syntax
+  unbundle no floor_ceiling_syntax
+  unbundle no uminus_syntax
 
 This is more robust than individual 'no_syntax' / 'no_notation'
 commands, which need to copy mixfix declarations from elsewhere and thus
diff -r 6ce0c8d59f5a -r ec121999a9cb src/FOL/IFOL.thy
--- a/src/FOL/IFOL.thy	Sun Oct 06 22:56:07 2024 +0200
+++ b/src/FOL/IFOL.thy	Tue Oct 08 12:10:35 2024 +0200
@@ -82,7 +82,7 @@
 
 definition \<open>True \<equiv> False \<longrightarrow> False\<close>
 
-definition Not (\<open>\<not> _\<close> [40] 40)
+definition Not (\<open>(\<open>open_block notation=\<open>prefix \<not>\<close>\<close>\<not> _)\<close> [40] 40)
   where not_def: \<open>\<not> P \<equiv> P \<longrightarrow> False\<close>
 
 definition iff  (infixr \<open>\<longleftrightarrow>\<close> 25)
diff -r 6ce0c8d59f5a -r ec121999a9cb src/FOLP/IFOLP.thy
--- a/src/FOLP/IFOLP.thy	Sun Oct 06 22:56:07 2024 +0200
+++ b/src/FOLP/IFOLP.thy	Tue Oct 08 12:10:35 2024 +0200
@@ -155,7 +155,7 @@
 
 (**** Definitions ****)
 
-definition Not :: "o => o"  (\<open>~ _\<close> [40] 40)
+definition Not :: "o => o"  (\<open>(\<open>open_block notation=\<open>prefix ~\<close>\<close>~ _)\<close> [40] 40)
   where not_def: "~P == P-->False"
 
 definition iff :: "[o,o] => o"  (infixr \<open><->\<close> 25)
diff -r 6ce0c8d59f5a -r ec121999a9cb src/HOL/Archimedean_Field.thy
--- a/src/HOL/Archimedean_Field.thy	Sun Oct 06 22:56:07 2024 +0200
+++ b/src/HOL/Archimedean_Field.thy	Tue Oct 08 12:10:35 2024 +0200
@@ -205,7 +205,7 @@
 subsection \<open>Floor function\<close>
 
 class floor_ceiling = archimedean_field +
-  fixes floor :: "'a \<Rightarrow> int"  (\<open>\<lfloor>_\<rfloor>\<close>)
+  fixes floor :: "'a \<Rightarrow> int"  (\<open>(\<open>open_block notation=\<open>mixfix floor\<close>\<close>\<lfloor>_\<rfloor>)\<close>)
   assumes floor_correct: "of_int \<lfloor>x\<rfloor> \<le> x \<and> x < of_int (\<lfloor>x\<rfloor> + 1)"
 
 lemma floor_unique: "of_int z \<le> x \<Longrightarrow> x < of_int z + 1 \<Longrightarrow> \<lfloor>x\<rfloor> = z"
@@ -427,7 +427,7 @@
 
 subsection \<open>Ceiling function\<close>
 
-definition ceiling :: "'a::floor_ceiling \<Rightarrow> int"  (\<open>\<lceil>_\<rceil>\<close>)
+definition ceiling :: "'a::floor_ceiling \<Rightarrow> int"  (\<open>(\<open>open_block notation=\<open>mixfix ceiling\<close>\<close>\<lceil>_\<rceil>)\<close>)
   where "\<lceil>x\<rceil> = - \<lfloor>- x\<rfloor>"
 
 lemma ceiling_correct: "of_int \<lceil>x\<rceil> - 1 < x \<and> x \<le> of_int \<lceil>x\<rceil>"
@@ -861,4 +861,10 @@
   finally show ?thesis .
 qed
 
+bundle floor_ceiling_syntax
+begin
+notation floor  (\<open>(\<open>open_block notation=\<open>mixfix floor\<close>\<close>\<lfloor>_\<rfloor>)\<close>)
+  and ceiling  (\<open>(\<open>open_block notation=\<open>mixfix ceiling\<close>\<close>\<lceil>_\<rceil>)\<close>)
 end
+
+end
diff -r 6ce0c8d59f5a -r ec121999a9cb src/HOL/BNF_Cardinal_Order_Relation.thy
--- a/src/HOL/BNF_Cardinal_Order_Relation.thy	Sun Oct 06 22:56:07 2024 +0200
+++ b/src/HOL/BNF_Cardinal_Order_Relation.thy	Tue Oct 08 12:10:35 2024 +0200
@@ -117,7 +117,7 @@
 We shall prove that this notion is unique up to order isomorphism, meaning
 that order isomorphism shall be the true identity of cardinals.\<close>
 
-definition card_of :: "'a set \<Rightarrow> 'a rel" (\<open>|_|\<close> )
+definition card_of :: "'a set \<Rightarrow> 'a rel" (\<open>(\<open>open_block notation=\<open>mixfix card_of\<close>\<close>|_|)\<close>)
   where "card_of A = (SOME r. card_order_on A r)"
 
 lemma card_of_card_order_on: "card_order_on A |A|"
diff -r 6ce0c8d59f5a -r ec121999a9cb src/HOL/BNF_Def.thy
--- a/src/HOL/BNF_Def.thy	Sun Oct 06 22:56:07 2024 +0200
+++ b/src/HOL/BNF_Def.thy	Tue Oct 08 12:10:35 2024 +0200
@@ -84,7 +84,7 @@
 lemma collect_comp: "collect F \<circ> g = collect ((\<lambda>f. f \<circ> g) ` F)"
   by (rule ext) (simp add: collect_def)
 
-definition convol (\<open>\<langle>(_,/ _)\<rangle>\<close>) where
+definition convol (\<open>(\<open>indent=1 notation=\<open>mixfix convol\<close>\<close>\<langle>_,/ _\<rangle>)\<close>) where
   "\<langle>f, g\<rangle> \<equiv> \<lambda>a. (f a, g a)"
 
 lemma fst_convol: "fst \<circ> \<langle>f, g\<rangle> = f"
diff -r 6ce0c8d59f5a -r ec121999a9cb src/HOL/Boolean_Algebras.thy
--- a/src/HOL/Boolean_Algebras.thy	Sun Oct 06 22:56:07 2024 +0200
+++ b/src/HOL/Boolean_Algebras.thy	Tue Oct 08 12:10:35 2024 +0200
@@ -14,7 +14,7 @@
 locale abstract_boolean_algebra = conj: abel_semigroup \<open>(\<^bold>\<sqinter>)\<close> + disj: abel_semigroup \<open>(\<^bold>\<squnion>)\<close>
   for conj :: \<open>'a \<Rightarrow> 'a \<Rightarrow> 'a\<close>  (infixr \<open>\<^bold>\<sqinter>\<close> 70)
     and disj :: \<open>'a \<Rightarrow> 'a \<Rightarrow> 'a\<close>  (infixr \<open>\<^bold>\<squnion>\<close> 65) +
-  fixes compl :: \<open>'a \<Rightarrow> 'a\<close>  (\<open>\<^bold>- _\<close> [81] 80)
+  fixes compl :: \<open>'a \<Rightarrow> 'a\<close>  (\<open>(\<open>open_block notation=\<open>prefix \<^bold>-\<close>\<close>\<^bold>- _)\<close> [81] 80)
     and zero :: \<open>'a\<close>  (\<open>\<^bold>0\<close>)
     and one  :: \<open>'a\<close>  (\<open>\<^bold>1\<close>)
   assumes conj_disj_distrib: \<open>x \<^bold>\<sqinter> (y \<^bold>\<squnion> z) = (x \<^bold>\<sqinter> y) \<^bold>\<squnion> (x \<^bold>\<sqinter> z)\<close>
diff -r 6ce0c8d59f5a -r ec121999a9cb src/HOL/Complete_Lattices.thy
--- a/src/HOL/Complete_Lattices.thy	Sun Oct 06 22:56:07 2024 +0200
+++ b/src/HOL/Complete_Lattices.thy	Tue Oct 08 12:10:35 2024 +0200
@@ -15,10 +15,10 @@
 subsection \<open>Syntactic infimum and supremum operations\<close>
 
 class Inf =
-  fixes Inf :: "'a set \<Rightarrow> 'a"  (\<open>\<Sqinter> _\<close> [900] 900)
+  fixes Inf :: "'a set \<Rightarrow> 'a"  (\<open>(\<open>open_block notation=\<open>prefix \<Sqinter>\<close>\<close>\<Sqinter> _)\<close> [900] 900)
 
 class Sup =
-  fixes Sup :: "'a set \<Rightarrow> 'a"  (\<open>\<Squnion> _\<close> [900] 900)
+  fixes Sup :: "'a set \<Rightarrow> 'a"  (\<open>(\<open>open_block notation=\<open>prefix \<Squnion>\<close>\<close>\<Squnion> _)\<close> [900] 900)
 
 syntax
   "_INF1"     :: "pttrns \<Rightarrow> 'b \<Rightarrow> 'b"           (\<open>(\<open>indent=3 notation=\<open>binder INF\<close>\<close>INF _./ _)\<close> [0, 10] 10)
diff -r 6ce0c8d59f5a -r ec121999a9cb src/HOL/Fun.thy
--- a/src/HOL/Fun.thy	Sun Oct 06 22:56:07 2024 +0200
+++ b/src/HOL/Fun.thy	Tue Oct 08 12:10:35 2024 +0200
@@ -844,7 +844,8 @@
   "_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>_/'((2_)')\<close> [1000, 0] 900)
+  "_Update"  :: "'a \<Rightarrow> updbinds \<Rightarrow> 'a"
+    (\<open>(\<open>open_block notation=\<open>mixfix function update\<close>\<close>_/'((2_)'))\<close> [1000, 0] 900)
 
 translations
   "_Update f (_updbinds b bs)" \<rightleftharpoons> "_Update (_Update f b) bs"
diff -r 6ce0c8d59f5a -r ec121999a9cb src/HOL/GCD.thy
--- a/src/HOL/GCD.thy	Sun Oct 06 22:56:07 2024 +0200
+++ b/src/HOL/GCD.thy	Tue Oct 08 12:10:35 2024 +0200
@@ -2851,7 +2851,7 @@
 definition (in semiring_1) semiring_char :: "'a itself \<Rightarrow> nat" 
   where "semiring_char _ = Gcd {n. of_nat n = (0 :: 'a)}"
 
-syntax "_type_char" :: "type => nat" (\<open>(\<open>indent=1 notation=\<open>prefix CHAR\<close>\<close>CHAR/(1'(_')))\<close>)
+syntax "_type_char" :: "type => nat" (\<open>(\<open>indent=1 notation=\<open>mixfix CHAR\<close>\<close>CHAR/(1'(_')))\<close>)
 syntax_consts "_type_char" \<rightleftharpoons> semiring_char
 translations "CHAR('t)" \<rightharpoonup> "CONST semiring_char (CONST Pure.type :: 't itself)"
 print_translation \<open>
diff -r 6ce0c8d59f5a -r ec121999a9cb src/HOL/Groups.thy
--- a/src/HOL/Groups.thy	Sun Oct 06 22:56:07 2024 +0200
+++ b/src/HOL/Groups.thy	Tue Oct 08 12:10:35 2024 +0200
@@ -198,11 +198,16 @@
   fixes minus :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"  (infixl \<open>-\<close> 65)
 
 class uminus =
-  fixes uminus :: "'a \<Rightarrow> 'a"  (\<open>- _\<close> [81] 80)
+  fixes uminus :: "'a \<Rightarrow> 'a"  (\<open>(\<open>open_block notation=\<open>prefix -\<close>\<close>- _)\<close> [81] 80)
 
 class times =
   fixes times :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"  (infixl \<open>*\<close> 70)
 
+bundle uminus_syntax
+begin
+notation uminus  (\<open>(\<open>open_block notation=\<open>prefix -\<close>\<close>- _)\<close> [81] 80)
+end
+
 
 subsection \<open>Semigroups and Monoids\<close>
 
@@ -1164,7 +1169,12 @@
 end
 
 class abs =
-  fixes abs :: "'a \<Rightarrow> 'a"  (\<open>\<bar>_\<bar>\<close>)
+  fixes abs :: "'a \<Rightarrow> 'a"  (\<open>(\<open>open_block notation=\<open>mixfix abs\<close>\<close>\<bar>_\<bar>)\<close>)
+
+bundle abs_syntax
+begin
+notation abs  (\<open>(\<open>open_block notation=\<open>mixfix abs\<close>\<close>\<bar>_\<bar>)\<close>)
+end
 
 class sgn =
   fixes sgn :: "'a \<Rightarrow> 'a"
diff -r 6ce0c8d59f5a -r ec121999a9cb src/HOL/Groups_Big.thy
--- a/src/HOL/Groups_Big.thy	Sun Oct 06 22:56:07 2024 +0200
+++ b/src/HOL/Groups_Big.thy	Tue Oct 08 12:10:35 2024 +0200
@@ -1415,7 +1415,7 @@
 sublocale prod: comm_monoid_set times 1
   defines prod = prod.F and prod' = prod.G ..
 
-abbreviation Prod (\<open>\<Prod>_\<close> [1000] 999)
+abbreviation Prod (\<open>(\<open>open_block notation=\<open>prefix \<Prod>\<close>\<close>\<Prod>_)\<close> [1000] 999)
   where "\<Prod>A \<equiv> prod (\<lambda>x. x) A"
 
 end
diff -r 6ce0c8d59f5a -r ec121999a9cb src/HOL/HOL.thy
--- a/src/HOL/HOL.thy	Sun Oct 06 22:56:07 2024 +0200
+++ b/src/HOL/HOL.thy	Tue Oct 08 12:10:35 2024 +0200
@@ -109,7 +109,7 @@
 definition False :: bool
   where "False \<equiv> (\<forall>P. P)"
 
-definition Not :: "bool \<Rightarrow> bool"  (\<open>\<not> _\<close> [40] 40)
+definition Not :: "bool \<Rightarrow> bool"  (\<open>(\<open>open_block notation=\<open>prefix \<not>\<close>\<close>\<not> _)\<close> [40] 40)
   where not_def: "\<not> P \<equiv> P \<longrightarrow> False"
 
 definition conj :: "[bool, bool] \<Rightarrow> bool"  (infixr \<open>\<and>\<close> 35)
@@ -169,7 +169,7 @@
   where "x \<noteq> y \<equiv> \<not> (x = y)"
 
 notation (ASCII)
-  Not  (\<open>~ _\<close> [40] 40) and
+  Not  (\<open>(\<open>open_block notation=\<open>prefix ~\<close>\<close>~ _)\<close> [40] 40) and
   conj  (infixr \<open>&\<close> 35) and
   disj  (infixr \<open>|\<close> 30) and
   implies  (infixr \<open>-->\<close> 25) and
@@ -191,11 +191,13 @@
 nonterminal case_syn and cases_syn
 syntax
   "_case_syntax" :: "['a, cases_syn] \<Rightarrow> 'b"  (\<open>(\<open>notation=\<open>mixfix case expression\<close>\<close>case _ of/ _)\<close> 10)
-  "_case1" :: "['a, 'b] \<Rightarrow> case_syn"  (\<open>(\<open>indent=2 notation=\<open>mixfix case clause\<close>\<close>_ \<Rightarrow>/ _)\<close> 10)
+  "_case1" :: "['a, 'b] \<Rightarrow> case_syn"
+    (\<open>(\<open>indent=2 notation=\<open>mixfix case clause\<close>\<close>(\<open>open_block notation=\<open>pattern case\<close>\<close>_) \<Rightarrow>/ _)\<close> 10)
   "" :: "case_syn \<Rightarrow> cases_syn"  (\<open>_\<close>)
   "_case2" :: "[case_syn, cases_syn] \<Rightarrow> cases_syn"  (\<open>_/ | _\<close>)
 syntax (ASCII)
-  "_case1" :: "['a, 'b] \<Rightarrow> case_syn"  (\<open>(\<open>indent=2 notation=\<open>mixfix case clause\<close>\<close>_ =>/ _)\<close> 10)
+  "_case1" :: "['a, 'b] \<Rightarrow> case_syn"
+    (\<open>(\<open>indent=2 notation=\<open>mixfix case clause\<close>\<close>(\<open>open_block notation=\<open>pattern case\<close>\<close>_) =>/ _)\<close> 10)
 
 notation (ASCII)
   All  (binder \<open>ALL \<close> 10) and
diff -r 6ce0c8d59f5a -r ec121999a9cb src/HOL/List.thy
--- a/src/HOL/List.thy	Sun Oct 06 22:56:07 2024 +0200
+++ b/src/HOL/List.thy	Tue Oct 08 12:10:35 2024 +0200
@@ -136,10 +136,11 @@
 nonterminal lupdbinds and lupdbind
 
 syntax
-  "_lupdbind":: "['a, 'a] => lupdbind"    (\<open>(\<open>indent=2 notation=\<open>mixfix list update\<close>\<close>_ :=/ _)\<close>)
+  "_lupdbind":: "['a, 'a] => lupdbind"    (\<open>(\<open>indent=2 notation=\<open>mixfix update\<close>\<close>_ :=/ _)\<close>)
   "" :: "lupdbind => lupdbinds"    (\<open>_\<close>)
   "_lupdbinds" :: "[lupdbind, lupdbinds] => lupdbinds"    (\<open>_,/ _\<close>)
-  "_LUpdate" :: "['a, lupdbinds] => 'a"    (\<open>_/[(_)]\<close> [1000,0] 900)
+  "_LUpdate" :: "['a, lupdbinds] => 'a"
+    (\<open>(\<open>open_block notation=\<open>mixfix list update\<close>\<close>_/[(_)])\<close> [1000,0] 900)
 
 translations
   "_LUpdate xs (_lupdbinds b bs)" == "_LUpdate (_LUpdate xs b) bs"
diff -r 6ce0c8d59f5a -r ec121999a9cb src/HOL/Main.thy
--- a/src/HOL/Main.thy	Sun Oct 06 22:56:07 2024 +0200
+++ b/src/HOL/Main.thy	Tue Oct 08 12:10:35 2024 +0200
@@ -36,11 +36,11 @@
   ordLeq3 (infix \<open>\<le>o\<close> 50) and
   ordLess2 (infix \<open><o\<close> 50) and
   ordIso2 (infix \<open>=o\<close> 50) and
-  card_of (\<open>|_|\<close>) and
+  card_of (\<open>(\<open>open_block notation=\<open>mixfix card_of\<close>\<close>|_|)\<close>) and
   BNF_Cardinal_Arithmetic.csum (infixr \<open>+c\<close> 65) and
   BNF_Cardinal_Arithmetic.cprod (infixr \<open>*c\<close> 80) and
   BNF_Cardinal_Arithmetic.cexp (infixr \<open>^c\<close> 90) and
-  BNF_Def.convol (\<open>\<langle>(_,/ _)\<rangle>\<close>)
+  BNF_Def.convol (\<open>(\<open>indent=1 notation=\<open>mixfix convol\<close>\<close>\<langle>_,/ _\<rangle>)\<close>)
 
 bundle cardinal_syntax
 begin
@@ -50,7 +50,7 @@
   ordLeq3 (infix \<open>\<le>o\<close> 50) and
   ordLess2 (infix \<open><o\<close> 50) and
   ordIso2 (infix \<open>=o\<close> 50) and
-  card_of (\<open>|_|\<close>) and
+  card_of (\<open>(\<open>open_block notation=\<open>mixfix card_of\<close>\<close>|_|)\<close>) and
   BNF_Cardinal_Arithmetic.csum (infixr \<open>+c\<close> 65) and
   BNF_Cardinal_Arithmetic.cprod (infixr \<open>*c\<close> 80) and
   BNF_Cardinal_Arithmetic.cexp (infixr \<open>^c\<close> 90)
@@ -73,8 +73,8 @@
   top  (\<open>\<top>\<close>) and
   inf  (infixl \<open>\<sqinter>\<close> 70) and
   sup  (infixl \<open>\<squnion>\<close> 65) and
-  Inf  (\<open>\<Sqinter> _\<close> [900] 900) and
-  Sup  (\<open>\<Squnion> _\<close> [900] 900)
+  Inf  (\<open>(\<open>open_block notation=\<open>prefix \<Sqinter>\<close>\<close>\<Sqinter> _)\<close> [900] 900) and
+  Sup  (\<open>(\<open>open_block notation=\<open>prefix \<Squnion>\<close>\<close>\<Squnion> _)\<close> [900] 900)
 
 syntax
   "_INF1"     :: "pttrns \<Rightarrow> 'b \<Rightarrow> 'b"           (\<open>(\<open>indent=3 notation=\<open>binder \<Sqinter>\<close>\<close>\<Sqinter>_./ _)\<close> [0, 10] 10)
diff -r 6ce0c8d59f5a -r ec121999a9cb src/HOL/Map.thy
--- a/src/HOL/Map.thy	Sun Oct 06 22:56:07 2024 +0200
+++ b/src/HOL/Map.thy	Tue Oct 08 12:10:35 2024 +0200
@@ -57,15 +57,15 @@
 nonterminal maplet and maplets
 
 syntax
-  "_maplet"  :: "['a, 'a] \<Rightarrow> maplet"             (\<open>_ /\<mapsto>/ _\<close>)
-  ""         :: "maplet \<Rightarrow> updbind"              (\<open>_\<close>)
-  ""         :: "maplet \<Rightarrow> maplets"             (\<open>_\<close>)
-  "_Maplets" :: "[maplet, maplets] \<Rightarrow> maplets" (\<open>_,/ _\<close>)
-  "_Map"     :: "maplets \<Rightarrow> 'a \<rightharpoonup> 'b"           (\<open>(\<open>indent=1 notation=\<open>mixfix maplets\<close>\<close>[_])\<close>)
+  "_maplet"  :: "['a, 'a] \<Rightarrow> maplet"  (\<open>(\<open>open_block notation=\<open>mixfix maplet\<close>\<close>_ /\<mapsto>/ _)\<close>)
+  ""         :: "maplet \<Rightarrow> updbind"  (\<open>_\<close>)
+  ""         :: "maplet \<Rightarrow> maplets"  (\<open>_\<close>)
+  "_Maplets" :: "[maplet, maplets] \<Rightarrow> maplets"  (\<open>_,/ _\<close>)
+  "_Map"     :: "maplets \<Rightarrow> 'a \<rightharpoonup> 'b"  (\<open>(\<open>indent=1 notation=\<open>mixfix map\<close>\<close>[_])\<close>)
 (* Syntax forbids \<open>[\<dots>, x := y, \<dots>]\<close> by introducing \<open>maplets\<close> in addition to \<open>updbinds\<close> *)
 
 syntax (ASCII)
-  "_maplet"  :: "['a, 'a] \<Rightarrow> maplet"             (\<open>_ /|->/ _\<close>)
+  "_maplet"  :: "['a, 'a] \<Rightarrow> maplet"  (\<open>(\<open>open_block notation=\<open>mixfix maplet\<close>\<close>_ /|->/ _)\<close>)
 
 syntax_consts
   "_maplet" "_Maplets" "_Map" \<rightleftharpoons> fun_upd
@@ -97,10 +97,10 @@
 text \<open>There is also the more specialized update syntax \<open>xs [\<mapsto>] ys\<close> for lists \<open>xs\<close> and \<open>ys\<close>.\<close>
 
 syntax
-  "_maplets"  :: "['a, 'a] \<Rightarrow> maplet"             (\<open>_ /[\<mapsto>]/ _\<close>)
+  "_maplets"  :: "['a, 'a] \<Rightarrow> maplet"  (\<open>(\<open>open_block notation=\<open>mixfix maplet\<close>\<close>_ /[\<mapsto>]/ _)\<close>)
 
 syntax (ASCII)
-  "_maplets" :: "['a, 'a] \<Rightarrow> maplet"             (\<open>_ /[|->]/ _\<close>)
+  "_maplets" :: "['a, 'a] \<Rightarrow> maplet"  (\<open>(\<open>open_block notation=\<open>mixfix maplet\<close>\<close>_ /[|->]/ _)\<close>)
 
 syntax_consts
   "_maplets" \<rightleftharpoons> map_upds
diff -r 6ce0c8d59f5a -r ec121999a9cb src/HOL/Nominal/Examples/Fsub.thy
--- a/src/HOL/Nominal/Examples/Fsub.thy	Sun Oct 06 22:56:07 2024 +0200
+++ b/src/HOL/Nominal/Examples/Fsub.thy	Tue Oct 08 12:10:35 2024 +0200
@@ -17,7 +17,7 @@
 section \<open>Types for Names, Nominal Datatype Declaration for Types and Terms\<close>
 
 no_syntax
-  "_Map" :: "maplets => 'a \<rightharpoonup> 'b"  (\<open>(\<open>indent=1 notation=\<open>mixfix maplets\<close>\<close>[_])\<close>)
+  "_Map" :: "maplets => 'a \<rightharpoonup> 'b"  (\<open>(\<open>indent=1 notation=\<open>mixfix map\<close>\<close>[_])\<close>)
 
 text \<open>The main point of this solution is to use names everywhere (be they bound, 
   binding or free). In System \FSUB{} there are two kinds of names corresponding to 
diff -r 6ce0c8d59f5a -r ec121999a9cb src/HOL/Nominal/Examples/Pattern.thy
--- a/src/HOL/Nominal/Examples/Pattern.thy	Sun Oct 06 22:56:07 2024 +0200
+++ b/src/HOL/Nominal/Examples/Pattern.thy	Tue Oct 08 12:10:35 2024 +0200
@@ -5,7 +5,7 @@
 begin
 
 no_syntax
-  "_Map" :: "maplets => 'a \<rightharpoonup> 'b"  (\<open>(\<open>indent=1 notation=\<open>mixfix maplets\<close>\<close>[_])\<close>)
+  "_Map" :: "maplets => 'a \<rightharpoonup> 'b"  (\<open>(\<open>indent=1 notation=\<open>mixfix map\<close>\<close>[_])\<close>)
 
 atom_decl name
 
diff -r 6ce0c8d59f5a -r ec121999a9cb src/HOL/Product_Type.thy
--- a/src/HOL/Product_Type.thy	Sun Oct 06 22:56:07 2024 +0200
+++ b/src/HOL/Product_Type.thy	Tue Oct 08 12:10:35 2024 +0200
@@ -289,10 +289,10 @@
   "_tuple"      :: "'a \<Rightarrow> tuple_args \<Rightarrow> 'a \<times> 'b"        (\<open>(\<open>indent=1 notation=\<open>mixfix tuple\<close>\<close>'(_,/ _'))\<close>)
   "_tuple_arg"  :: "'a \<Rightarrow> tuple_args"                   (\<open>_\<close>)
   "_tuple_args" :: "'a \<Rightarrow> tuple_args \<Rightarrow> tuple_args"     (\<open>_,/ _\<close>)
-  "_pattern"    :: "pttrn \<Rightarrow> patterns \<Rightarrow> pttrn"         (\<open>'(_,/ _')\<close>)
+  "_pattern"    :: "pttrn \<Rightarrow> patterns \<Rightarrow> pttrn"         (\<open>(\<open>open_block notation=\<open>pattern tuple\<close>\<close>'(_,/ _'))\<close>)
   ""            :: "pttrn \<Rightarrow> patterns"                  (\<open>_\<close>)
   "_patterns"   :: "pttrn \<Rightarrow> patterns \<Rightarrow> patterns"      (\<open>_,/ _\<close>)
-  "_unit"       :: pttrn                                (\<open>'(')\<close>)
+  "_unit"       :: pttrn                                (\<open>(\<open>open_block notation=\<open>pattern unit\<close>\<close>'('))\<close>)
 syntax_consts
   "_pattern" "_patterns" \<rightleftharpoons> case_prod and
   "_unit" \<rightleftharpoons> case_unit
diff -r 6ce0c8d59f5a -r ec121999a9cb src/HOL/Record.thy
--- a/src/HOL/Record.thy	Sun Oct 06 22:56:07 2024 +0200
+++ b/src/HOL/Record.thy	Tue Oct 08 12:10:35 2024 +0200
@@ -430,25 +430,25 @@
   ""                    :: "field_type => field_types"          (\<open>_\<close>)
   "_field_types"        :: "field_type => field_types => field_types"    (\<open>_,/ _\<close>)
   "_record_type"        :: "field_types => type"                (\<open>(\<open>indent=3 notation=\<open>mixfix record type\<close>\<close>\<lparr>_\<rparr>)\<close>)
-  "_record_type_scheme" :: "field_types => type => type"        (\<open>(\<open>indent=3 notation=\<open>mixfix record type\<close>\<close>\<lparr>_,/ (2\<dots> ::/ _)\<rparr>)\<close>)
+  "_record_type_scheme" :: "field_types => type => type"        (\<open>(\<open>indent=3 notation=\<open>mixfix record type\<close>\<close>\<lparr>_,/ (\<open>indent=2 notation=\<open>infix more type\<close>\<close>\<dots> ::/ _)\<rparr>)\<close>)
 
   "_field"              :: "ident => 'a => field"               (\<open>(\<open>indent=2 notation=\<open>infix field value\<close>\<close>_ =/ _)\<close>)
   ""                    :: "field => fields"                    (\<open>_\<close>)
   "_fields"             :: "field => fields => fields"          (\<open>_,/ _\<close>)
   "_record"             :: "fields => 'a"                       (\<open>(\<open>indent=3 notation=\<open>mixfix record value\<close>\<close>\<lparr>_\<rparr>)\<close>)
-  "_record_scheme"      :: "fields => 'a => 'a"                 (\<open>(\<open>indent=3 notation=\<open>mixfix record value\<close>\<close>\<lparr>_,/ (2\<dots> =/ _)\<rparr>)\<close>)
+  "_record_scheme"      :: "fields => 'a => 'a"                 (\<open>(\<open>indent=3 notation=\<open>mixfix record value\<close>\<close>\<lparr>_,/ (\<open>indent=2 notation=\<open>infix more value\<close>\<close>\<dots> =/ _)\<rparr>)\<close>)
 
   "_field_update"       :: "ident => 'a => field_update"        (\<open>(\<open>indent=2 notation=\<open>infix field update\<close>\<close>_ :=/ _)\<close>)
   ""                    :: "field_update => field_updates"      (\<open>_\<close>)
   "_field_updates"      :: "field_update => field_updates => field_updates"  (\<open>_,/ _\<close>)
-  "_record_update"      :: "'a => field_updates => 'b"          (\<open>_/(\<open>indent=3 notation=\<open>mixfix record update\<close>\<close>\<lparr>_\<rparr>)\<close> [900, 0] 900)
+  "_record_update"      :: "'a => field_updates => 'b"          (\<open>(\<open>open_block notation=\<open>mixfix record update\<close>\<close>_/(3\<lparr>_\<rparr>))\<close> [900, 0] 900)
 
 syntax (ASCII)
   "_record_type"        :: "field_types => type"                (\<open>(\<open>indent=3 notation=\<open>mixfix record type\<close>\<close>'(| _ |'))\<close>)
-  "_record_type_scheme" :: "field_types => type => type"        (\<open>(\<open>indent=3 notation=\<open>mixfix record type\<close>\<close>'(| _,/ (2... ::/ _) |'))\<close>)
+  "_record_type_scheme" :: "field_types => type => type"        (\<open>(\<open>indent=3 notation=\<open>mixfix record type\<close>\<close>'(| _,/ (\<open>indent=2 notation=\<open>infix more type\<close>\<close>... ::/ _) |'))\<close>)
   "_record"             :: "fields => 'a"                       (\<open>(\<open>indent=3 notation=\<open>mixfix record value\<close>\<close>'(| _ |'))\<close>)
-  "_record_scheme"      :: "fields => 'a => 'a"                 (\<open>(\<open>indent=3 notation=\<open>mixfix record value\<close>\<close>'(| _,/ (2... =/ _) |'))\<close>)
-  "_record_update"      :: "'a => field_updates => 'b"          (\<open>_/(\<open>indent=3 notation=\<open>mixfix record update\<close>\<close>'(| _ |'))\<close> [900, 0] 900)
+  "_record_scheme"      :: "fields => 'a => 'a"                 (\<open>(\<open>indent=3 notation=\<open>mixfix record value\<close>\<close>'(| _,/ (\<open>indent=2 notation=\<open>infix more value\<close>\<close>... =/ _) |'))\<close>)
+  "_record_update"      :: "'a => field_updates => 'b"          (\<open>(\<open>open_block notation=\<open>mixfix record update\<close>\<close>_/(3'(| _ |')))\<close> [900, 0] 900)
 
 
 subsection \<open>Record package\<close>
diff -r 6ce0c8d59f5a -r ec121999a9cb src/HOL/Typerep.thy
--- a/src/HOL/Typerep.thy	Sun Oct 06 22:56:07 2024 +0200
+++ b/src/HOL/Typerep.thy	Tue Oct 08 12:10:35 2024 +0200
@@ -18,7 +18,7 @@
 end
 
 syntax
-  "_TYPEREP" :: "type => logic"  (\<open>(\<open>indent=1 notation=\<open>prefix TYPEREP\<close>\<close>TYPEREP/(1'(_')))\<close>)
+  "_TYPEREP" :: "type => logic"  (\<open>(\<open>indent=1 notation=\<open>mixfix TYPEREP\<close>\<close>TYPEREP/(1'(_')))\<close>)
 syntax_consts
   "_TYPEREP" \<rightleftharpoons> typerep
 
diff -r 6ce0c8d59f5a -r ec121999a9cb src/Pure/PIDE/markup_kind.ML
--- a/src/Pure/PIDE/markup_kind.ML	Sun Oct 06 22:56:07 2024 +0200
+++ b/src/Pure/PIDE/markup_kind.ML	Tue Oct 08 12:10:35 2024 +0200
@@ -22,6 +22,7 @@
   val markup_postfix: Markup.T
   val markup_infix: Markup.T
   val markup_binder: Markup.T
+  val markup_pattern: Markup.T
   val markup_type_literal: Markup.T
   val markup_literal: Markup.T
   val markup_type_application: Markup.T
@@ -102,6 +103,7 @@
 val markup_postfix = setup_notation (Binding.make ("postfix", \<^here>));
 val markup_infix = setup_notation (Binding.make ("infix", \<^here>));
 val markup_binder = setup_notation (Binding.make ("binder", \<^here>));
+val markup_pattern = setup_notation (Binding.make ("pattern", \<^here>));
 val markup_type_literal = setup_notation (Binding.make ("type_literal", \<^here>));
 val markup_literal = setup_notation (Binding.make ("literal", \<^here>));
 
diff -r 6ce0c8d59f5a -r ec121999a9cb src/Pure/pure_thy.ML
--- a/src/Pure/pure_thy.ML	Sun Oct 06 22:56:07 2024 +0200
+++ b/src/Pure/pure_thy.ML	Tue Oct 08 12:10:35 2024 +0200
@@ -153,14 +153,16 @@
     ("",            typ "var_position \<Rightarrow> aprop",       Mixfix.mixfix "_"),
     ("_DDDOT",      typ "aprop",                       Mixfix.mixfix "\<dots>"),
     ("_aprop",      typ "aprop \<Rightarrow> prop",
-      Mixfix.mixfix "(\<open>open_block notation=\<open>mixfix atomic prop\<close>\<close>PROP _)"),
+      Mixfix.mixfix "(\<open>open_block notation=\<open>prefix PROP\<close>\<close>PROP _)"),
     ("_asm",        typ "prop \<Rightarrow> asms",                Mixfix.mixfix "_"),
     ("_asms",       typ "prop \<Rightarrow> asms \<Rightarrow> asms",        Mixfix.mixfix "_;/ _"),
     ("_bigimpl",    typ "asms \<Rightarrow> prop \<Rightarrow> prop",
       mixfix ("(\<open>notation=\<open>infix \<Longrightarrow>\<close>\<close>(1\<lbrakk>_\<rbrakk>)/ \<Longrightarrow> _)", [0, 1], 1)),
-    ("_ofclass",    typ "type \<Rightarrow> logic \<Rightarrow> prop",       Mixfix.mixfix "(1OFCLASS/(1'(_,/ _')))"),
+    ("_ofclass",    typ "type \<Rightarrow> logic \<Rightarrow> prop",
+      Mixfix.mixfix "(\<open>indent=1 notation=\<open>mixfix OFCLASS\<close>\<close>OFCLASS/(1'(_,/ _')))"),
     ("_mk_ofclass", typ "dummy",                       NoSyn),
-    ("_TYPE",       typ "type \<Rightarrow> logic",               Mixfix.mixfix "(1TYPE/(1'(_')))"),
+    ("_TYPE",       typ "type \<Rightarrow> logic",
+      Mixfix.mixfix "(\<open>indent=1 notation=\<open>mixfix TYPE\<close>\<close>TYPE/(1'(_')))"),
     ("",            typ "id_position \<Rightarrow> logic",        Mixfix.mixfix "_"),
     ("",            typ "longid_position \<Rightarrow> logic",    Mixfix.mixfix "_"),
     ("",            typ "var_position \<Rightarrow> logic",       Mixfix.mixfix "_"),
@@ -185,17 +187,27 @@
     ("_position",   typ "string_token \<Rightarrow> string_position", Mixfix.mixfix "_"),
     ("_position",   typ "cartouche \<Rightarrow> cartouche_position", Mixfix.mixfix "_"),
     ("_type_constraint_", typ "'a",                    NoSyn),
-    ("_context_const", typ "id_position \<Rightarrow> logic",     Mixfix.mixfix "CONST _"),
-    ("_context_const", typ "id_position \<Rightarrow> aprop",     Mixfix.mixfix "CONST _"),
-    ("_context_const", typ "longid_position \<Rightarrow> logic", Mixfix.mixfix "CONST _"),
-    ("_context_const", typ "longid_position \<Rightarrow> aprop", Mixfix.mixfix "CONST _"),
-    ("_context_xconst", typ "id_position \<Rightarrow> logic",    Mixfix.mixfix "XCONST _"),
-    ("_context_xconst", typ "id_position \<Rightarrow> aprop",    Mixfix.mixfix "XCONST _"),
-    ("_context_xconst", typ "longid_position \<Rightarrow> logic", Mixfix.mixfix "XCONST _"),
-    ("_context_xconst", typ "longid_position \<Rightarrow> aprop", Mixfix.mixfix "XCONST _"),
+    ("_context_const", typ "id_position \<Rightarrow> logic",
+      Mixfix.mixfix "(\<open>open_block notation=\<open>prefix CONST\<close>\<close>CONST _)"),
+    ("_context_const", typ "id_position \<Rightarrow> aprop",
+      Mixfix.mixfix "(\<open>open_block notation=\<open>prefix CONST\<close>\<close>CONST _)"),
+    ("_context_const", typ "longid_position \<Rightarrow> logic",
+      Mixfix.mixfix "(\<open>open_block notation=\<open>prefix CONST\<close>\<close>CONST _)"),
+    ("_context_const", typ "longid_position \<Rightarrow> aprop",
+      Mixfix.mixfix "(\<open>open_block notation=\<open>prefix CONST\<close>\<close>CONST _)"),
+    ("_context_xconst", typ "id_position \<Rightarrow> logic",
+      Mixfix.mixfix "(\<open>open_block notation=\<open>prefix XCONST\<close>\<close>XCONST _)"),
+    ("_context_xconst", typ "id_position \<Rightarrow> aprop",
+      Mixfix.mixfix "(\<open>open_block notation=\<open>prefix XCONST\<close>\<close>XCONST _)"),
+    ("_context_xconst", typ "longid_position \<Rightarrow> logic",
+      Mixfix.mixfix "(\<open>open_block notation=\<open>prefix XCONST\<close>\<close>XCONST _)"),
+    ("_context_xconst", typ "longid_position \<Rightarrow> aprop",
+      Mixfix.mixfix "(\<open>open_block notation=\<open>prefix XCONST\<close>\<close>XCONST _)"),
     (const "Pure.dummy_pattern", typ "aprop",          Mixfix.mixfix "'_"),
-    ("_sort_constraint", typ "type \<Rightarrow> prop",           Mixfix.mixfix "(1SORT'_CONSTRAINT/(1'(_')))"),
-    (const "Pure.term", typ "logic \<Rightarrow> prop",           Mixfix.mixfix "TERM _"),
+    ("_sort_constraint", typ "type \<Rightarrow> prop",
+      Mixfix.mixfix "(\<open>indent=1 notation=\<open>mixfix SORT_CONSTRAINT\<close>\<close>SORT'_CONSTRAINT/(1'(_')))"),
+    (const "Pure.term", typ "logic \<Rightarrow> prop",
+      Mixfix.mixfix "(\<open>open_block notation=\<open>prefix TERM\<close>\<close>TERM _)"),
     (const "Pure.conjunction", typ "prop \<Rightarrow> prop \<Rightarrow> prop", infixr_ ("&&&", 2))]
   #> Sign.syntax_global true Syntax.mode_default applC_syntax
   #> Sign.syntax_global true (Print_Mode.ASCII, true)
diff -r 6ce0c8d59f5a -r ec121999a9cb src/Sequents/ILL.thy
--- a/src/Sequents/ILL.thy	Sun Oct 06 22:56:07 2024 +0200
+++ b/src/Sequents/ILL.thy	Tue Oct 08 12:10:35 2024 +0200
@@ -48,7 +48,7 @@
 definition liff :: "[o, o] \<Rightarrow> o"  (infixr \<open>o-o\<close> 45)
   where "P o-o Q == (P -o Q) >< (Q -o P)"
 
-definition aneg :: "o\<Rightarrow>o"  (\<open>~_\<close>)
+definition aneg :: "o\<Rightarrow>o"  (\<open>(\<open>open_block notation=\<open>prefix ~\<close>\<close>~_)\<close>)
   where "~A == A -o 0"
 
 
diff -r 6ce0c8d59f5a -r ec121999a9cb src/Sequents/LK0.thy
--- a/src/Sequents/LK0.thy	Sun Oct 06 22:56:07 2024 +0200
+++ b/src/Sequents/LK0.thy	Tue Oct 08 12:10:35 2024 +0200
@@ -24,7 +24,7 @@
   True         :: o
   False        :: o
   equal        :: "['a,'a] \<Rightarrow> o"     (infixl \<open>=\<close> 50)
-  Not          :: "o \<Rightarrow> o"           (\<open>\<not> _\<close> [40] 40)
+  Not          :: "o \<Rightarrow> o"           (\<open>(\<open>open_block notation=\<open>prefix \<not>\<close>\<close>\<not> _)\<close> [40] 40)
   conj         :: "[o,o] \<Rightarrow> o"       (infixr \<open>\<and>\<close> 35)
   disj         :: "[o,o] \<Rightarrow> o"       (infixr \<open>\<or>\<close> 30)
   imp          :: "[o,o] \<Rightarrow> o"       (infixr \<open>\<longrightarrow>\<close> 25)
diff -r 6ce0c8d59f5a -r ec121999a9cb src/ZF/Cardinal.thy
--- a/src/ZF/Cardinal.thy	Sun Oct 06 22:56:07 2024 +0200
+++ b/src/ZF/Cardinal.thy	Tue Oct 08 12:10:35 2024 +0200
@@ -25,8 +25,8 @@
     "A \<prec> B \<equiv> A \<lesssim> B \<and> \<not>(A \<approx> B)"
 
 definition
-  cardinal :: "i\<Rightarrow>i"           (\<open>|_|\<close>)  where
-    "|A| \<equiv> (\<mu> i. i \<approx> A)"
+  cardinal :: "i\<Rightarrow>i"  (\<open>(\<open>open_block notation=\<open>mixfix cardinal\<close>\<close>|_|)\<close>)
+  where "|A| \<equiv> (\<mu> i. i \<approx> A)"
 
 definition
   Finite   :: "i\<Rightarrow>o"  where
diff -r 6ce0c8d59f5a -r ec121999a9cb src/ZF/Constructible/Normal.thy
--- a/src/ZF/Constructible/Normal.thy	Sun Oct 06 22:56:07 2024 +0200
+++ b/src/ZF/Constructible/Normal.thy	Tue Oct 08 12:10:35 2024 +0200
@@ -463,7 +463,7 @@
 numbers.\<close>
 
 definition
-  Aleph :: "i \<Rightarrow> i"  (\<open>\<aleph>_\<close> [90] 90) where
+  Aleph :: "i \<Rightarrow> i"  (\<open>(\<open>open_block notation=\<open>prefix \<aleph>\<close>\<close>\<aleph>_)\<close> [90] 90) where
     "Aleph(a) \<equiv> transrec2(a, nat, \<lambda>x r. csucc(r))"
 
 lemma Card_Aleph [simp, intro]:
diff -r 6ce0c8d59f5a -r ec121999a9cb src/ZF/Induct/Multiset.thy
--- a/src/ZF/Induct/Multiset.thy	Sun Oct 06 22:56:07 2024 +0200
+++ b/src/ZF/Induct/Multiset.thy	Tue Oct 08 12:10:35 2024 +0200
@@ -53,7 +53,7 @@
 
 definition
   (* set of elements of a multiset *)
-  msingle :: "i \<Rightarrow> i"    (\<open>{#_#}\<close>)  where
+  msingle :: "i \<Rightarrow> i"    (\<open>(\<open>open_block notation=\<open>mixfix multiset\<close>\<close>{#_#})\<close>)  where
   "{#a#} \<equiv> {\<langle>a, 1\<rangle>}"
 
 definition
diff -r 6ce0c8d59f5a -r ec121999a9cb src/ZF/Int.thy
--- a/src/ZF/Int.thy	Sun Oct 06 22:56:07 2024 +0200
+++ b/src/ZF/Int.thy	Tue Oct 08 12:10:35 2024 +0200
@@ -17,8 +17,8 @@
     "int \<equiv> (nat*nat)//intrel"
 
 definition
-  int_of :: "i\<Rightarrow>i" \<comment> \<open>coercion from nat to int\<close>    (\<open>$# _\<close> [80] 80)  where
-    "$# m \<equiv> intrel `` {<natify(m), 0>}"
+  int_of :: "i\<Rightarrow>i" \<comment> \<open>coercion from nat to int\<close>  (\<open>(\<open>open_block notation=\<open>prefix $#\<close>\<close>$# _)\<close> [80] 80)
+  where "$# m \<equiv> intrel `` {<natify(m), 0>}"
 
 definition
   intify :: "i\<Rightarrow>i" \<comment> \<open>coercion from ANYTHING to int\<close>  where
@@ -29,8 +29,8 @@
     "raw_zminus(z) \<equiv> \<Union>\<langle>x,y\<rangle>\<in>z. intrel``{\<langle>y,x\<rangle>}"
 
 definition
-  zminus :: "i\<Rightarrow>i"                                 (\<open>$- _\<close> [80] 80)  where
-    "$- z \<equiv> raw_zminus (intify(z))"
+  zminus :: "i\<Rightarrow>i"  (\<open>(\<open>open_block notation=\<open>prefix $-\<close>\<close>$- _)\<close> [80] 80)
+  where "$- z \<equiv> raw_zminus (intify(z))"
 
 definition
   znegative   ::      "i\<Rightarrow>o"  where
diff -r 6ce0c8d59f5a -r ec121999a9cb src/ZF/OrdQuant.thy
--- a/src/ZF/OrdQuant.thy	Sun Oct 06 22:56:07 2024 +0200
+++ b/src/ZF/OrdQuant.thy	Tue Oct 08 12:10:35 2024 +0200
@@ -330,7 +330,7 @@
 subsubsection\<open>Sets as Classes\<close>
 
 definition
-  setclass :: "[i,i] \<Rightarrow> o"       (\<open>##_\<close> [40] 40)  where
+  setclass :: "[i,i] \<Rightarrow> o"  (\<open>(\<open>open_block notation=\<open>prefix setclass\<close>\<close>##_)\<close> [40] 40)  where
    "setclass(A) \<equiv> \<lambda>x. x \<in> A"
 
 lemma setclass_iff [simp]: "setclass(A,x) <-> x \<in> A"
diff -r 6ce0c8d59f5a -r ec121999a9cb src/ZF/QPair.thy
--- a/src/ZF/QPair.thy	Sun Oct 06 22:56:07 2024 +0200
+++ b/src/ZF/QPair.thy	Tue Oct 08 12:10:35 2024 +0200
@@ -21,8 +21,8 @@
 \<close>
 
 definition
-  QPair     :: "[i, i] \<Rightarrow> i"                      (\<open><(_;/ _)>\<close>)  where
-    "<a;b> \<equiv> a+b"
+  QPair     :: "[i, i] \<Rightarrow> i"  (\<open>(\<open>indent=1 notation=\<open>mixfix Quine pair\<close>\<close><_;/ _>)\<close>)
+  where "<a;b> \<equiv> a+b"
 
 definition
   qfst :: "i \<Rightarrow> i"  where
diff -r 6ce0c8d59f5a -r ec121999a9cb src/ZF/Trancl.thy
--- a/src/ZF/Trancl.thy	Sun Oct 06 22:56:07 2024 +0200
+++ b/src/ZF/Trancl.thy	Tue Oct 08 12:10:35 2024 +0200
@@ -32,7 +32,7 @@
     "trans(r) \<equiv> \<forall>x y z. \<langle>x,y\<rangle>: r \<longrightarrow> \<langle>y,z\<rangle>: r \<longrightarrow> \<langle>x,z\<rangle>: r"
 
 definition
-  trans_on :: "[i,i]\<Rightarrow>o"  (\<open>trans[_]'(_')\<close>)  where
+  trans_on :: "[i,i]\<Rightarrow>o"  (\<open>(\<open>open_block notation=\<open>mixfix trans_on\<close>\<close>trans[_]'(_'))\<close>)  where
     "trans[A](r) \<equiv> \<forall>x\<in>A. \<forall>y\<in>A. \<forall>z\<in>A.
                           \<langle>x,y\<rangle>: r \<longrightarrow> \<langle>y,z\<rangle>: r \<longrightarrow> \<langle>x,z\<rangle>: r"
 
diff -r 6ce0c8d59f5a -r ec121999a9cb src/ZF/UNITY/Increasing.thy
--- a/src/ZF/UNITY/Increasing.thy	Sun Oct 06 22:56:07 2024 +0200
+++ b/src/ZF/UNITY/Increasing.thy	Tue Oct 08 12:10:35 2024 +0200
@@ -11,13 +11,15 @@
 theory Increasing imports Constrains Monotonicity begin
 
 definition
-  increasing :: "[i, i, i\<Rightarrow>i] \<Rightarrow> i" (\<open>increasing[_]'(_, _')\<close>)  where
+  increasing :: "[i, i, i\<Rightarrow>i] \<Rightarrow> i"  (\<open>(\<open>open_block notation=\<open>mixfix increasing\<close>\<close>increasing[_]'(_, _'))\<close>)
+  where
   "increasing[A](r, f) \<equiv>
     {F \<in> program. (\<forall>k \<in> A. F \<in> stable({s \<in> state. <k, f(s)> \<in> r})) \<and>
                 (\<forall>x \<in> state. f(x):A)}"
   
 definition
-  Increasing :: "[i, i, i\<Rightarrow>i] \<Rightarrow> i" (\<open>Increasing[_]'(_, _')\<close>)  where
+  Increasing :: "[i, i, i\<Rightarrow>i] \<Rightarrow> i" (\<open>(\<open>open_block notation=\<open>mixfix Increasing\<close>\<close>Increasing[_]'(_, _'))\<close>)
+  where
   "Increasing[A](r, f) \<equiv>
     {F \<in> program. (\<forall>k \<in> A. F \<in> Stable({s \<in> state. <k, f(s)> \<in> r})) \<and>
                 (\<forall>x \<in> state. f(x):A)}"
diff -r 6ce0c8d59f5a -r ec121999a9cb src/ZF/WF.thy
--- a/src/ZF/WF.thy	Sun Oct 06 22:56:07 2024 +0200
+++ b/src/ZF/WF.thy	Tue Oct 08 12:10:35 2024 +0200
@@ -24,7 +24,7 @@
     "wf(r) \<equiv> \<forall>Z. Z=0 | (\<exists>x\<in>Z. \<forall>y. \<langle>y,x\<rangle>:r \<longrightarrow> \<not> y \<in> Z)"
 
 definition
-  wf_on        :: "[i,i]\<Rightarrow>o"                      (\<open>wf[_]'(_')\<close>)  where
+  wf_on :: "[i,i]\<Rightarrow>o"  (\<open>(\<open>open_block notation=\<open>mixfix wf_on\<close>\<close>wf[_]'(_'))\<close>)  where
     (*r is well-founded on A*)
     "wf_on(A,r) \<equiv> wf(r \<inter> A*A)"
 
@@ -46,8 +46,8 @@
     "wfrec(r,a,H) \<equiv> wftrec(r^+, a, \<lambda>x f. H(x, restrict(f,r-``{x})))"
 
 definition
-  wfrec_on     :: "[i, i, i, [i,i]\<Rightarrow>i] \<Rightarrow>i"       (\<open>wfrec[_]'(_,_,_')\<close>)  where
-    "wfrec[A](r,a,H) \<equiv> wfrec(r \<inter> A*A, a, H)"
+  wfrec_on :: "[i, i, i, [i,i]\<Rightarrow>i] \<Rightarrow>i"  (\<open>(\<open>open_block notation=\<open>mixfix wfrec_on\<close>\<close>wfrec[_]'(_,_,_'))\<close>)
+  where "wfrec[A](r,a,H) \<equiv> wfrec(r \<inter> A*A, a, H)"
 
 
 subsection\<open>Well-Founded Relations\<close>
diff -r 6ce0c8d59f5a -r ec121999a9cb src/ZF/ZF_Base.thy
--- a/src/ZF/ZF_Base.thy	Sun Oct 06 22:56:07 2024 +0200
+++ b/src/ZF/ZF_Base.thy	Tue Oct 08 12:10:35 2024 +0200
@@ -20,7 +20,7 @@
   and zero :: "i"  (\<open>0\<close>)  \<comment> \<open>the empty set\<close>
   and Pow :: "i \<Rightarrow> i"  \<comment> \<open>power sets\<close>
   and Inf :: "i"  \<comment> \<open>infinite set\<close>
-  and Union :: "i \<Rightarrow> i"  (\<open>\<Union>_\<close> [90] 90)
+  and Union :: "i \<Rightarrow> i"  (\<open>(\<open>open_block notation=\<open>prefix \<Union>\<close>\<close>\<Union>_)\<close> [90] 90)
   and PrimReplace :: "[i, [i, i] \<Rightarrow> o] \<Rightarrow> i"
 
 abbreviation not_mem :: "[i, i] \<Rightarrow> o"  (infixl \<open>\<notin>\<close> 50)  \<comment> \<open>negated membership relation\<close>
@@ -83,7 +83,7 @@
 
 subsection \<open>General union and intersection\<close>
 
-definition Inter :: "i \<Rightarrow> i"  (\<open>\<Inter>_\<close> [90] 90)
+definition Inter :: "i \<Rightarrow> i"  (\<open>(\<open>open_block notation=\<open>prefix \<Inter>\<close>\<close>\<Inter>_)\<close> [90] 90)
   where "\<Inter>(A) \<equiv> { x\<in>\<Union>(A) . \<forall>y\<in>A. x\<in>y}"
 
 syntax
@@ -196,8 +196,8 @@
 (* Patterns -- extends pre-defined type "pttrn" used in abstractions *)
 nonterminal patterns
 syntax
-  "_pattern"  :: "patterns \<Rightarrow> pttrn"         (\<open>\<langle>_\<rangle>\<close>)
-  ""          :: "pttrn \<Rightarrow> patterns"         (\<open>_\<close>)
+  "_pattern"  :: "patterns \<Rightarrow> pttrn"  (\<open>(\<open>open_block notation=\<open>pattern tuple\<close>\<close>\<langle>_\<rangle>)\<close>)
+  ""          :: "pttrn \<Rightarrow> patterns"  (\<open>_\<close>)
   "_patterns" :: "[pttrn, patterns] \<Rightarrow> patterns"  (\<open>_,/_\<close>)
 syntax_consts
   "_pattern" "_patterns" == split
@@ -297,7 +297,7 @@
   "_PROD"     :: "[pttrn, i, i] \<Rightarrow> i"        (\<open>(\<open>indent=3 notation=\<open>binder PROD:\<close>\<close>PROD _:_./ _)\<close> 10)
   "_SUM"      :: "[pttrn, i, i] \<Rightarrow> i"        (\<open>(\<open>indent=3 notation=\<open>binder SUM:\<close>\<close>SUM _:_./ _)\<close> 10)
   "_lam"      :: "[pttrn, i, i] \<Rightarrow> i"        (\<open>(\<open>indent=3 notation=\<open>binder lam:\<close>\<close>lam _:_./ _)\<close> 10)
-  "_Tuple"    :: "[i, tuple_args] \<Rightarrow> i"      (\<open><(_,/ _)>\<close>)
+  "_Tuple"    :: "[i, tuple_args] \<Rightarrow> i"      (\<open>(\<open>indent=1 notation=\<open>mixfix tuple enumeration\<close>\<close><_,/ _>)\<close>)
   "_pattern"  :: "patterns \<Rightarrow> pttrn"         (\<open><_>\<close>)
 
 
diff -r 6ce0c8d59f5a -r ec121999a9cb src/ZF/func.thy
--- a/src/ZF/func.thy	Sun Oct 06 22:56:07 2024 +0200
+++ b/src/ZF/func.thy	Tue Oct 08 12:10:35 2024 +0200
@@ -448,10 +448,10 @@
 nonterminal updbinds and updbind
 
 syntax
-  "_updbind"    :: "[i, i] \<Rightarrow> updbind"               (\<open>(\<open>indent=2 notation=\<open>infix update\<close>\<close>_ :=/ _)\<close>)
-  ""            :: "updbind \<Rightarrow> updbinds"             (\<open>_\<close>)
-  "_updbinds"   :: "[updbind, updbinds] \<Rightarrow> updbinds" (\<open>_,/ _\<close>)
-  "_Update"     :: "[i, updbinds] \<Rightarrow> i"              (\<open>_/'((_)')\<close> [900,0] 900)
+  "_updbind"    :: "[i, i] \<Rightarrow> updbind"  (\<open>(\<open>indent=2 notation=\<open>infix update\<close>\<close>_ :=/ _)\<close>)
+  ""            :: "updbind \<Rightarrow> updbinds"  (\<open>_\<close>)
+  "_updbinds"   :: "[updbind, updbinds] \<Rightarrow> updbinds"  (\<open>_,/ _\<close>)
+  "_Update"     :: "[i, updbinds] \<Rightarrow> i"  (\<open>(\<open>open_block notation=\<open>mixfix function update\<close>\<close>_/'((_)'))\<close> [900,0] 900)
 translations
   "_Update (f, _updbinds(b,bs))"  == "_Update (_Update(f,b), bs)"
   "f(x:=y)"                       == "CONST update(f,x,y)"