# HG changeset patch
# User wenzelm
# Date 1726868220 -7200
# Node ID 2a77bc3b4eacc58661586bcb24138b9817be78f4
# Parent  01b8c8d17f1362a7b8c71ddc44d924cca13674ad
more inner syntax markup: minor object-logics;

diff -r 01b8c8d17f13 -r 2a77bc3b4eac src/CCL/CCL.thy
--- a/src/CCL/CCL.thy	Fri Sep 20 23:36:33 2024 +0200
+++ b/src/CCL/CCL.thy	Fri Sep 20 23:37:00 2024 +0200
@@ -35,7 +35,7 @@
   (*** Term Formers ***)
   true        ::       "i"
   false       ::       "i"
-  pair        ::       "[i,i]\<Rightarrow>i"             (\<open>(1<_,/_>)\<close>)
+  pair        ::       "[i,i]\<Rightarrow>i"             (\<open>(\<open>indent=1 notation=\<open>mixfix pair\<close>\<close><_,/_>)\<close>)
   lambda      ::       "(i\<Rightarrow>i)\<Rightarrow>i"            (binder \<open>lam \<close> 55)
   "case"      ::       "[i,i,i,[i,i]\<Rightarrow>i,(i\<Rightarrow>i)\<Rightarrow>i]\<Rightarrow>i"
   "apply"     ::       "[i,i]\<Rightarrow>i"             (infixl \<open>`\<close> 56)
diff -r 01b8c8d17f13 -r 2a77bc3b4eac src/CCL/Set.thy
--- a/src/CCL/Set.thy	Fri Sep 20 23:36:33 2024 +0200
+++ b/src/CCL/Set.thy	Fri Sep 20 23:37:00 2024 +0200
@@ -18,7 +18,7 @@
   and set_extension: "A = B \<longleftrightarrow> (ALL x. x:A \<longleftrightarrow> x:B)"
 
 syntax
-  "_Coll" :: "[idt, o] \<Rightarrow> 'a set"  (\<open>(1{_./ _})\<close>)
+  "_Coll" :: "[idt, o] \<Rightarrow> 'a set"  (\<open>(\<open>indent=1 notation=\<open>mixfix Collect\<close>\<close>{_./ _})\<close>)
 syntax_consts
   "_Coll" == Collect
 translations
@@ -50,8 +50,8 @@
   where "Bex(A, P) == EX x. x:A \<and> P(x)"
 
 syntax
-  "_Ball" :: "[idt, 'a set, o] \<Rightarrow> o"  (\<open>(ALL _:_./ _)\<close> [0, 0, 0] 10)
-  "_Bex" :: "[idt, 'a set, o] \<Rightarrow> o"  (\<open>(EX _:_./ _)\<close> [0, 0, 0] 10)
+  "_Ball" :: "[idt, 'a set, o] \<Rightarrow> o"  (\<open>(\<open>notation=\<open>binder ALL:\<close>\<close>ALL _:_./ _)\<close> [0, 0, 0] 10)
+  "_Bex" :: "[idt, 'a set, o] \<Rightarrow> o"  (\<open>(\<open>notation=\<open>binder EX:\<close>\<close>EX _:_./ _)\<close> [0, 0, 0] 10)
 syntax_consts
   "_Ball" == Ball and
   "_Bex" == Bex
@@ -127,8 +127,8 @@
   where "UNION(A, B) == {y. EX x:A. y: B(x)}"
 
 syntax
-  "_INTER" :: "[idt, 'a set, 'b set] \<Rightarrow> 'b set"  (\<open>(INT _:_./ _)\<close> [0, 0, 0] 10)
-  "_UNION" :: "[idt, 'a set, 'b set] \<Rightarrow> 'b set"  (\<open>(UN _:_./ _)\<close> [0, 0, 0] 10)
+  "_INTER" :: "[idt, 'a set, 'b set] \<Rightarrow> 'b set"  (\<open>(\<open>notation=\<open>binder INT:\<close>\<close>INT _:_./ _)\<close> [0, 0, 0] 10)
+  "_UNION" :: "[idt, 'a set, 'b set] \<Rightarrow> 'b set"  (\<open>(\<open>notation=\<open>binder UN:\<close>\<close>UN _:_./ _)\<close> [0, 0, 0] 10)
 syntax_consts
   "_INTER" == INTER and
   "_UNION" == UNION
diff -r 01b8c8d17f13 -r 2a77bc3b4eac src/CCL/Term.thy
--- a/src/CCL/Term.thy	Fri Sep 20 23:36:33 2024 +0200
+++ b/src/CCL/Term.thy	Fri Sep 20 23:37:00 2024 +0200
@@ -12,7 +12,8 @@
 definition one :: "i"
   where "one == true"
 
-definition "if" :: "[i,i,i]\<Rightarrow>i"  (\<open>(3if _/ then _/ else _)\<close> [0,0,60] 60)
+definition "if" :: "[i,i,i]\<Rightarrow>i"
+    (\<open>(\<open>indent=3 notation=\<open>mixfix if then else\<close>\<close>if _/ then _/ else _)\<close> [0,0,60] 60)
   where "if b then t else u  == case(b, t, u, \<lambda> x y. bot, \<lambda>v. bot)"
 
 definition inl :: "i\<Rightarrow>i"
@@ -48,7 +49,8 @@
 definition "let1" :: "[i,i\<Rightarrow>i]\<Rightarrow>i"
   where let_def: "let1(t, f) == case(t,f(true),f(false), \<lambda>x y. f(<x,y>), \<lambda>u. f(lam x. u(x)))"
 
-syntax "_let1" :: "[idt,i,i]\<Rightarrow>i"  (\<open>(3let _ be _/ in _)\<close> [0,0,60] 60)
+syntax "_let1" :: "[idt,i,i]\<Rightarrow>i"
+  (\<open>(\<open>indent=3 notation=\<open>mixfix let be in\<close>\<close>let _ be _/ in _)\<close> [0,0,60] 60)
 syntax_consts "_let1" == let1
 translations "let x be a in e" == "CONST let1(a, \<lambda>x. e)"
 
@@ -65,9 +67,12 @@
       \<lambda>g'. f(\<lambda>x y z. g'(<x,<y,z>>)))"
 
 syntax
-  "_letrec" :: "[idt,idt,i,i]\<Rightarrow>i"  (\<open>(3letrec _ _ be _/ in _)\<close> [0,0,0,60] 60)
-  "_letrec2" :: "[idt,idt,idt,i,i]\<Rightarrow>i"  (\<open>(3letrec _ _ _ be _/ in _)\<close> [0,0,0,0,60] 60)
-  "_letrec3" :: "[idt,idt,idt,idt,i,i]\<Rightarrow>i"  (\<open>(3letrec _ _ _ _ be _/ in _)\<close> [0,0,0,0,0,60] 60)
+  "_letrec" :: "[idt,idt,i,i]\<Rightarrow>i"
+    (\<open>(\<open>indent=3 notation=\<open>mixfix letrec be in\<close>\<close>letrec _ _ be _/ in _)\<close> [0,0,0,60] 60)
+  "_letrec2" :: "[idt,idt,idt,i,i]\<Rightarrow>i"
+    (\<open>(\<open>indent=3 notation=\<open>mixfix letrec be in\<close>\<close>letrec _ _ _ be _/ in _)\<close> [0,0,0,0,60] 60)
+  "_letrec3" :: "[idt,idt,idt,idt,i,i]\<Rightarrow>i"
+    (\<open>(\<open>indent=3 notation=\<open>mixfix letrec be in\<close>\<close>letrec _ _ _ _ be _/ in _)\<close> [0,0,0,0,0,60] 60)
 syntax_consts
   "_letrec" == letrec and
   "_letrec2" == letrec2 and
@@ -143,7 +148,7 @@
 definition lrec :: "[i,i,[i,i,i]\<Rightarrow>i]\<Rightarrow>i"
   where "lrec(l,b,c) == letrec g x be lcase(x, b, \<lambda>h t. c(h,t,g(t))) in g(l)"
 
-definition napply :: "[i\<Rightarrow>i,i,i]\<Rightarrow>i"  (\<open>(_ ^ _ ` _)\<close> [56,56,56] 56)
+definition napply :: "[i\<Rightarrow>i,i,i]\<Rightarrow>i"  (\<open>(\<open>notation=\<open>mixfix napply\<close>\<close>_ ^ _ ` _)\<close> [56,56,56] 56)
   where "f ^n` a == nrec(n,a,\<lambda>x g. f(g))"
 
 lemmas simp_can_defs = one_def inl_def inr_def
diff -r 01b8c8d17f13 -r 2a77bc3b4eac src/CCL/Trancl.thy
--- a/src/CCL/Trancl.thy	Fri Sep 20 23:36:33 2024 +0200
+++ b/src/CCL/Trancl.thy	Fri Sep 20 23:37:00 2024 +0200
@@ -18,10 +18,10 @@
 definition relcomp :: "[i set,i set] \<Rightarrow> i set"  (infixr \<open>O\<close> 60)  (*composition of relations*)
   where "r O s == {xz. EX x y z. xz = <x,z> \<and> <x,y>:s \<and> <y,z>:r}"
 
-definition rtrancl :: "i set \<Rightarrow> i set"  (\<open>(_^*)\<close> [100] 100)
+definition rtrancl :: "i set \<Rightarrow> i set"  (\<open>(\<open>notation=\<open>postfix ^*\<close>\<close>_^*)\<close> [100] 100)
   where "r^* == lfp(\<lambda>s. id Un (r O s))"
 
-definition trancl :: "i set \<Rightarrow> i set"  (\<open>(_^+)\<close> [100] 100)
+definition trancl :: "i set \<Rightarrow> i set"  (\<open>(\<open>notation=\<open>postfix ^+\<close>\<close>_^+)\<close> [100] 100)
   where "r^+ == r O rtrancl(r)"
 
 
diff -r 01b8c8d17f13 -r 2a77bc3b4eac src/CCL/Type.thy
--- a/src/CCL/Type.thy	Fri Sep 20 23:36:33 2024 +0200
+++ b/src/CCL/Type.thy	Fri Sep 20 23:37:00 2024 +0200
@@ -13,7 +13,7 @@
   where "Subtype(A, P) == {x. x:A \<and> P(x)}"
 
 syntax
-  "_Subtype" :: "[idt, 'a set, o] \<Rightarrow> 'a set"  (\<open>(1{_: _ ./ _})\<close>)
+  "_Subtype" :: "[idt, 'a set, o] \<Rightarrow> 'a set"  (\<open>(\<open>indent=1 notation=\<open>mixfix Subtype\<close>\<close>{_: _ ./ _})\<close>)
 syntax_consts
   "_Subtype" == Subtype
 translations
@@ -35,10 +35,10 @@
   where "Sigma(A,B) == {x. EX a:A. EX b:B(a).x=<a,b>}"
 
 syntax
-  "_Pi" :: "[idt, i set, i set] \<Rightarrow> i set"  (\<open>(3PROD _:_./ _)\<close> [0,0,60] 60)
-  "_Sigma" :: "[idt, i set, i set] \<Rightarrow> i set"  (\<open>(3SUM _:_./ _)\<close> [0,0,60] 60)
-  "_arrow" :: "[i set, i set] \<Rightarrow> i set"  (\<open>(_ ->/ _)\<close>  [54, 53] 53)
-  "_star"  :: "[i set, i set] \<Rightarrow> i set"  (\<open>(_ */ _)\<close> [56, 55] 55)
+  "_Pi" :: "[idt, i set, i set] \<Rightarrow> i set"  (\<open>(\<open>indent=3 notation=\<open>binder PROD:\<close>\<close>PROD _:_./ _)\<close> [0,0,60] 60)
+  "_Sigma" :: "[idt, i set, i set] \<Rightarrow> i set"  (\<open>(\<open>indent=3 notation=\<open>binder SUM:\<close>\<close>SUM _:_./ _)\<close> [0,0,60] 60)
+  "_arrow" :: "[i set, i set] \<Rightarrow> i set"  (\<open>(\<open>notation=\<open>infix ->\<close>\<close>_ ->/ _)\<close>  [54, 53] 53)
+  "_star"  :: "[i set, i set] \<Rightarrow> i set"  (\<open>(\<open>notation=\<open>infix *\<close>\<close>_ */ _)\<close> [56, 55] 55)
 syntax_consts
   "_Pi" "_arrow" \<rightleftharpoons> Pi and
   "_Sigma" "_star" \<rightleftharpoons> Sigma
@@ -73,7 +73,7 @@
 definition TEx :: "(i set \<Rightarrow> i set) \<Rightarrow> i set"  (binder \<open>TEX \<close> 55)
   where "TEX X. B(X) == Union({X. EX Y. X=B(Y)})"
 
-definition Lift :: "i set \<Rightarrow> i set"  (\<open>(3[_])\<close>)
+definition Lift :: "i set \<Rightarrow> i set"  (\<open>(\<open>indent=3 notation=\<open>mixfix Lift\<close>\<close>[_])\<close>)
   where "[A] == A Un {bot}"
 
 definition SPLIT :: "[i, [i, i] \<Rightarrow> i set] \<Rightarrow> i set"
diff -r 01b8c8d17f13 -r 2a77bc3b4eac src/CTT/CTT.thy
--- a/src/CTT/CTT.thy	Fri Sep 20 23:36:33 2024 +0200
+++ b/src/CTT/CTT.thy	Fri Sep 20 23:37:00 2024 +0200
@@ -18,10 +18,10 @@
 
 consts
   \<comment> \<open>Judgments\<close>
-  Type      :: "t \<Rightarrow> prop"          (\<open>(_ type)\<close> [10] 5)
-  Eqtype    :: "[t,t]\<Rightarrow>prop"        (\<open>(_ =/ _)\<close> [10,10] 5)
-  Elem      :: "[i, t]\<Rightarrow>prop"       (\<open>(_ /: _)\<close> [10,10] 5)
-  Eqelem    :: "[i,i,t]\<Rightarrow>prop"      (\<open>(_ =/ _ :/ _)\<close> [10,10,10] 5)
+  Type      :: "t \<Rightarrow> prop"          (\<open>(\<open>notation=\<open>postfix Type\<close>\<close>_ type)\<close> [10] 5)
+  Eqtype    :: "[t,t]\<Rightarrow>prop"        (\<open>(\<open>notation=\<open>infix Eqtype\<close>\<close>_ =/ _)\<close> [10,10] 5)
+  Elem      :: "[i, t]\<Rightarrow>prop"       (\<open>(\<open>notation=\<open>infix Elem\<close>\<close>_ /: _)\<close> [10,10] 5)
+  Eqelem    :: "[i,i,t]\<Rightarrow>prop"      (\<open>(\<open>notation=\<open>mixfix Eqelem\<close>\<close>_ =/ _ :/ _)\<close> [10,10,10] 5)
   Reduce    :: "[i,i]\<Rightarrow>prop"        (\<open>Reduce[_,_]\<close>)
   \<comment> \<open>Types for truth values\<close>
   F         :: "t"
@@ -40,7 +40,7 @@
   "when"    :: "[i, i\<Rightarrow>i, i\<Rightarrow>i]\<Rightarrow>i"
   \<comment> \<open>General sum and binary product\<close>
   Sum       :: "[t, i\<Rightarrow>t]\<Rightarrow>t"
-  pair      :: "[i,i]\<Rightarrow>i"           (\<open>(1<_,/_>)\<close>)
+  pair      :: "[i,i]\<Rightarrow>i"           (\<open>(\<open>indent=1 notation=\<open>mixfix pair\<close>\<close><_,/_>)\<close>)
   fst       :: "i\<Rightarrow>i"
   snd       :: "i\<Rightarrow>i"
   split     :: "[i, [i,i]\<Rightarrow>i] \<Rightarrow>i"
@@ -56,8 +56,8 @@
  must be introduced after the judgment forms.\<close>
 
 syntax
-  "_PROD"   :: "[idt,t,t]\<Rightarrow>t"       (\<open>(3\<Prod>_:_./ _)\<close> 10)
-  "_SUM"    :: "[idt,t,t]\<Rightarrow>t"       (\<open>(3\<Sum>_:_./ _)\<close> 10)
+  "_PROD"   :: "[idt,t,t]\<Rightarrow>t"       (\<open>(\<open>indent=3 notation=\<open>binder \<Prod>\<close>\<close>\<Prod>_:_./ _)\<close> 10)
+  "_SUM"    :: "[idt,t,t]\<Rightarrow>t"       (\<open>(\<open>indent=3 notation=\<open>binder \<Sum>\<close>\<close>\<Sum>_:_./ _)\<close> 10)
 syntax_consts
   "_PROD" \<rightleftharpoons> Prod and
   "_SUM" \<rightleftharpoons> Sum
diff -r 01b8c8d17f13 -r 2a77bc3b4eac src/Cube/Cube.thy
--- a/src/Cube/Cube.thy	Fri Sep 20 23:36:33 2024 +0200
+++ b/src/Cube/Cube.thy	Fri Sep 20 23:37:00 2024 +0200
@@ -29,15 +29,15 @@
 
 nonterminal context' and typing'
 syntax
-  "_Trueprop" :: "[context', typing'] \<Rightarrow> prop"  (\<open>(_/ \<turnstile> _)\<close>)
-  "_Trueprop1" :: "typing' \<Rightarrow> prop"  (\<open>(_)\<close>)
+  "_Trueprop" :: "[context', typing'] \<Rightarrow> prop"  (\<open>(\<open>notation=\<open>infix Trueprop\<close>\<close>_/ \<turnstile> _)\<close>)
+  "_Trueprop1" :: "typing' \<Rightarrow> prop"  (\<open>(\<open>notation=\<open>prefix Trueprop\<close>\<close>_)\<close>)
   "" :: "id \<Rightarrow> context'"  (\<open>_\<close>)
   "" :: "var \<Rightarrow> context'"  (\<open>_\<close>)
   "_MT_context" :: "context'"  (\<open>\<close>)
   "_Context" :: "[typing', context'] \<Rightarrow> context'"  (\<open>_ _\<close>)
-  "_Has_type" :: "[term, term] \<Rightarrow> typing'"  (\<open>(_:/ _)\<close> [0, 0] 5)
-  "_Lam" :: "[idt, term, term] \<Rightarrow> term"  (\<open>(3\<^bold>\<lambda>_:_./ _)\<close> [0, 0, 0] 10)
-  "_Pi" :: "[idt, term, term] \<Rightarrow> term"  (\<open>(3\<Prod>_:_./ _)\<close> [0, 0] 10)
+  "_Has_type" :: "[term, term] \<Rightarrow> typing'"  (\<open>(\<open>notation=\<open>infix Has_Type\<close>\<close>_:/ _)\<close> [0, 0] 5)
+  "_Lam" :: "[idt, term, term] \<Rightarrow> term"  (\<open>(\<open>indent=3 notation=\<open>binder \<^bold>\<lambda>\<close>\<close>\<^bold>\<lambda>_:_./ _)\<close> [0, 0, 0] 10)
+  "_Pi" :: "[idt, term, term] \<Rightarrow> term"  (\<open>(\<open>indent=3 notation=\<open>binder \<Prod>\<close>\<close>\<Prod>_:_./ _)\<close> [0, 0] 10)
   "_arrow" :: "[term, term] \<Rightarrow> term"  (infixr \<open>\<rightarrow>\<close> 10)
 syntax_consts
   "_Trueprop" \<rightleftharpoons> Trueprop and
diff -r 01b8c8d17f13 -r 2a77bc3b4eac src/FOL/IFOL.thy
--- a/src/FOL/IFOL.thy	Fri Sep 20 23:36:33 2024 +0200
+++ b/src/FOL/IFOL.thy	Fri Sep 20 23:37:00 2024 +0200
@@ -101,7 +101,7 @@
 abbreviation not_equal :: \<open>['a, 'a] \<Rightarrow> o\<close>  (infixl \<open>\<noteq>\<close> 50)
   where \<open>x \<noteq> y \<equiv> \<not> (x = y)\<close>
 
-syntax "_Uniq" :: "pttrn \<Rightarrow> o \<Rightarrow> o"  (\<open>(2\<exists>\<^sub>\<le>\<^sub>1 _./ _)\<close> [0, 10] 10)
+syntax "_Uniq" :: "pttrn \<Rightarrow> o \<Rightarrow> o"  (\<open>(\<open>indent=2 notation=\<open>binder \<exists>\<^sub>\<le>\<^sub>1\<close>\<close>\<exists>\<^sub>\<le>\<^sub>1 _./ _)\<close> [0, 10] 10)
 syntax_consts "_Uniq" \<rightleftharpoons> Uniq
 translations "\<exists>\<^sub>\<le>\<^sub>1x. P" \<rightleftharpoons> "CONST Uniq (\<lambda>x. P)"
 
@@ -743,10 +743,10 @@
   where \<open>Let(s, f) \<equiv> f(s)\<close>
 
 syntax
-  "_bind"       :: \<open>[pttrn, 'a] => letbind\<close>           (\<open>(2_ =/ _)\<close> 10)
+  "_bind"       :: \<open>[pttrn, 'a] => letbind\<close>  (\<open>(\<open>indent=2 notation=\<open>infix letbind\<close>\<close>_ =/ _)\<close> 10)
   ""            :: \<open>letbind => letbinds\<close>              (\<open>_\<close>)
   "_binds"      :: \<open>[letbind, letbinds] => letbinds\<close>  (\<open>_;/ _\<close>)
-  "_Let"        :: \<open>[letbinds, 'a] => 'a\<close>             (\<open>(let (_)/ in (_))\<close> 10)
+  "_Let"        :: \<open>[letbinds, 'a] => 'a\<close>  (\<open>(\<open>notation=\<open>mixfix let in\<close>\<close>let (_)/ in (_))\<close> 10)
 syntax_consts "_Let" \<rightleftharpoons> Let
 translations
   "_Let(_binds(b, bs), e)"  == "_Let(b, _Let(bs, e))"
diff -r 01b8c8d17f13 -r 2a77bc3b4eac src/FOLP/IFOLP.thy
--- a/src/FOLP/IFOLP.thy	Fri Sep 20 23:36:33 2024 +0200
+++ b/src/FOLP/IFOLP.thy	Fri Sep 20 23:37:00 2024 +0200
@@ -23,7 +23,7 @@
 consts
       (*** Judgements ***)
  Proof          ::   "[o,p]=>prop"
- EqProof        ::   "[p,p,o]=>prop"    (\<open>(3_ /= _ :/ _)\<close> [10,10,10] 5)
+ EqProof        ::   "[p,p,o]=>prop"  (\<open>(\<open>indent=3 notation=\<open>mixfix EqProof\<close>\<close>_ /= _ :/ _)\<close> [10,10,10] 5)
 
       (*** Logical Connectives -- Type Formers ***)
  eq             ::      "['a,'a] => o"  (infixl \<open>=\<close> 50)
@@ -44,7 +44,7 @@
  contr          :: "p=>p"
  fst            :: "p=>p"
  snd            :: "p=>p"
- pair           :: "[p,p]=>p"           (\<open>(1<_,/_>)\<close>)
+ pair           :: "[p,p]=>p"           (\<open>(\<open>indent=1 notation=\<open>mixfix pair\<close>\<close><_,/_>)\<close>)
  split          :: "[p, [p,p]=>p] =>p"
  inl            :: "p=>p"
  inr            :: "p=>p"
@@ -53,14 +53,14 @@
  App            :: "[p,p]=>p"           (infixl \<open>`\<close> 60)
  alll           :: "['a=>p]=>p"         (binder \<open>all \<close> 55)
  app            :: "[p,'a]=>p"          (infixl \<open>^\<close> 55)
- exists         :: "['a,p]=>p"          (\<open>(1[_,/_])\<close>)
+ exists         :: "['a,p]=>p"          (\<open>(\<open>indent=1 notation=\<open>mixfix exists\<close>\<close>[_,/_])\<close>)
  xsplit         :: "[p,['a,p]=>p]=>p"
  ideq           :: "'a=>p"
  idpeel         :: "[p,'a=>p]=>p"
  nrm            :: p
  NRM            :: p
 
-syntax "_Proof" :: "[p,o]=>prop"    (\<open>(_ /: _)\<close> [51, 10] 5)
+syntax "_Proof" :: "[p,o]=>prop"    (\<open>(\<open>notation=\<open>infix Proof\<close>\<close>_ /: _)\<close> [51, 10] 5)
 
 parse_translation \<open>
   let fun proof_tr [p, P] = Syntax.const \<^const_syntax>\<open>Proof\<close> $ P $ p
diff -r 01b8c8d17f13 -r 2a77bc3b4eac src/LCF/LCF.thy
--- a/src/LCF/LCF.thy	Fri Sep 20 23:36:33 2024 +0200
+++ b/src/LCF/LCF.thy	Fri Sep 20 23:37:00 2024 +0200
@@ -39,8 +39,8 @@
  WHEN   :: "['a\<Rightarrow>'c, 'b\<Rightarrow>'c, 'a+'b] \<Rightarrow> 'c"
  adm    :: "('a \<Rightarrow> o) \<Rightarrow> o"
  VOID   :: "void"               (\<open>'(')\<close>)
- PAIR   :: "['a,'b] \<Rightarrow> 'a*'b"   (\<open>(1<_,/_>)\<close> [0,0] 100)
- COND   :: "[tr,'a,'a] \<Rightarrow> 'a"   (\<open>(_ \<Rightarrow>/ (_ |/ _))\<close> [60,60,60] 60)
+ PAIR   :: "['a,'b] \<Rightarrow> 'a*'b"   (\<open>(\<open>indent=1 notation=\<open>mixfix PAIR\<close>\<close><_,/_>)\<close> [0,0] 100)
+ COND   :: "[tr,'a,'a] \<Rightarrow> 'a"   (\<open>(\<open>notation=\<open>mixfix COND\<close>\<close>_ \<Rightarrow>/ (_ |/ _))\<close> [60,60,60] 60)
  less   :: "['a,'a] \<Rightarrow> o"       (infixl \<open><<\<close> 50)
 
 axiomatization where
diff -r 01b8c8d17f13 -r 2a77bc3b4eac src/Sequents/ILL.thy
--- a/src/Sequents/ILL.thy	Fri Sep 20 23:36:33 2024 +0200
+++ b/src/Sequents/ILL.thy	Fri Sep 20 23:37:00 2024 +0200
@@ -29,8 +29,8 @@
   PromAux :: "three_seqi"
 
 syntax
-  "_Trueprop" :: "single_seqe" (\<open>((_)/ \<turnstile> (_))\<close> [6,6] 5)
-  "_Context"  :: "two_seqe"   (\<open>((_)/ :=: (_))\<close> [6,6] 5)
+  "_Trueprop" :: "single_seqe" (\<open>(\<open>notation=\<open>infix Trueprop\<close>\<close>(_)/ \<turnstile> (_))\<close> [6,6] 5)
+  "_Context"  :: "two_seqe"   (\<open>(\<open>notation=\<open>infix Context\<close>\<close>(_)/ :=: (_))\<close> [6,6] 5)
   "_PromAux"  :: "three_seqe" (\<open>promaux {_||_||_}\<close>)
 
 parse_translation \<open>
diff -r 01b8c8d17f13 -r 2a77bc3b4eac src/Sequents/LK0.thy
--- a/src/Sequents/LK0.thy	Fri Sep 20 23:36:33 2024 +0200
+++ b/src/Sequents/LK0.thy	Fri Sep 20 23:37:00 2024 +0200
@@ -34,7 +34,7 @@
   Ex           :: "('a \<Rightarrow> o) \<Rightarrow> o"   (binder \<open>\<exists>\<close> 10)
 
 syntax
- "_Trueprop"    :: "two_seqe" (\<open>((_)/ \<turnstile> (_))\<close> [6,6] 5)
+ "_Trueprop"    :: "two_seqe" (\<open>(\<open>notation=\<open>infix Trueprop\<close>\<close>(_)/ \<turnstile> (_))\<close> [6,6] 5)
 
 parse_translation \<open>[(\<^syntax_const>\<open>_Trueprop\<close>, K (two_seq_tr \<^const_syntax>\<open>Trueprop\<close>))]\<close>
 print_translation \<open>[(\<^const_syntax>\<open>Trueprop\<close>, K (two_seq_tr' \<^syntax_const>\<open>_Trueprop\<close>))]\<close>
@@ -104,7 +104,7 @@
   The: "\<lbrakk>$H \<turnstile> $E, P(a), $F;  \<And>x.$H, P(x) \<turnstile> $E, x=a, $F\<rbrakk> \<Longrightarrow>
          $H \<turnstile> $E, P(THE x. P(x)), $F"
 
-definition If :: "[o, 'a, 'a] \<Rightarrow> 'a" (\<open>(if (_)/ then (_)/ else (_))\<close> 10)
+definition If :: "[o, 'a, 'a] \<Rightarrow> 'a" (\<open>(\<open>notation=\<open>mixfix if then else\<close>\<close>if (_)/ then (_)/ else (_))\<close> 10)
   where "If(P,x,y) \<equiv> THE z::'a. (P \<longrightarrow> z = x) \<and> (\<not> P \<longrightarrow> z = y)"
 
 
diff -r 01b8c8d17f13 -r 2a77bc3b4eac src/ZF/Finite.thy
--- a/src/ZF/Finite.thy	Fri Sep 20 23:36:33 2024 +0200
+++ b/src/ZF/Finite.thy	Fri Sep 20 23:37:00 2024 +0200
@@ -19,7 +19,7 @@
 
 consts
   Fin       :: "i\<Rightarrow>i"
-  FiniteFun :: "[i,i]\<Rightarrow>i"         (\<open>(_ -||>/ _)\<close> [61, 60] 60)
+  FiniteFun :: "[i,i]\<Rightarrow>i"  (\<open>(\<open>notation=\<open>infix -||>\<close>\<close>_ -||>/ _)\<close> [61, 60] 60)
 
 inductive
   domains   "Fin(A)" \<subseteq> "Pow(A)"
diff -r 01b8c8d17f13 -r 2a77bc3b4eac src/ZF/Induct/Multiset.thy
--- a/src/ZF/Induct/Multiset.thy	Fri Sep 20 23:36:33 2024 +0200
+++ b/src/ZF/Induct/Multiset.thy	Fri Sep 20 23:37:00 2024 +0200
@@ -70,11 +70,11 @@
   "msize(M) \<equiv> setsum(\<lambda>a. $# mcount(M,a), mset_of(M))"
 
 abbreviation
-  melem :: "[i,i] \<Rightarrow> o"    (\<open>(_/ :# _)\<close> [50, 51] 50)  where
+  melem :: "[i,i] \<Rightarrow> o"    (\<open>(\<open>notation=\<open>infix :#\<close>\<close>_/ :# _)\<close> [50, 51] 50)  where
   "a :# M \<equiv> a \<in> mset_of(M)"
 
 syntax
-  "_MColl" :: "[pttrn, i, o] \<Rightarrow> i" (\<open>(1{# _ \<in> _./ _#})\<close>)
+  "_MColl" :: "[pttrn, i, o] \<Rightarrow> i" (\<open>(\<open>indent=1 notation=\<open>mixfix MCollect\<close>\<close>{# _ \<in> _./ _#})\<close>)
 syntax_consts "_MColl" \<rightleftharpoons> MCollect
 translations
   "{#x \<in> M. P#}" == "CONST MCollect(M, \<lambda>x. P)"
diff -r 01b8c8d17f13 -r 2a77bc3b4eac src/ZF/OrdQuant.thy
--- a/src/ZF/OrdQuant.thy	Fri Sep 20 23:36:33 2024 +0200
+++ b/src/ZF/OrdQuant.thy	Fri Sep 20 23:37:00 2024 +0200
@@ -23,9 +23,9 @@
     "OUnion(i,B) \<equiv> {z: \<Union>x\<in>i. B(x). Ord(i)}"
 
 syntax
-  "_oall"     :: "[idt, i, o] \<Rightarrow> o"        (\<open>(3\<forall>_<_./ _)\<close> 10)
-  "_oex"      :: "[idt, i, o] \<Rightarrow> o"        (\<open>(3\<exists>_<_./ _)\<close> 10)
-  "_OUNION"   :: "[idt, i, i] \<Rightarrow> i"        (\<open>(3\<Union>_<_./ _)\<close> 10)
+  "_oall"     :: "[idt, i, o] \<Rightarrow> o"  (\<open>(\<open>indent=3 notation=\<open>binder \<forall><\<close>\<close>\<forall>_<_./ _)\<close> 10)
+  "_oex"      :: "[idt, i, o] \<Rightarrow> o"  (\<open>(\<open>indent=3 notation=\<open>binder \<exists><\<close>\<close>\<exists>_<_./ _)\<close> 10)
+  "_OUNION"   :: "[idt, i, i] \<Rightarrow> i"  (\<open>(\<open>indent=3 notation=\<open>binder \<Union><\<close>\<close>\<Union>_<_./ _)\<close> 10)
 syntax_consts
   "_oall" \<rightleftharpoons> oall and
   "_oex" \<rightleftharpoons> oex and
@@ -196,8 +196,8 @@
     "rex(M, P) \<equiv> \<exists>x. M(x) \<and> P(x)"
 
 syntax
-  "_rall"     :: "[pttrn, i\<Rightarrow>o, o] \<Rightarrow> o"        (\<open>(3\<forall>_[_]./ _)\<close> 10)
-  "_rex"      :: "[pttrn, i\<Rightarrow>o, o] \<Rightarrow> o"        (\<open>(3\<exists>_[_]./ _)\<close> 10)
+  "_rall"     :: "[pttrn, i\<Rightarrow>o, o] \<Rightarrow> o"  (\<open>(\<open>indent=3 notation=\<open>binder \<forall>[]\<close>\<close>\<forall>_[_]./ _)\<close> 10)
+  "_rex"      :: "[pttrn, i\<Rightarrow>o, o] \<Rightarrow> o"  (\<open>(\<open>indent=3 notation=\<open>binder \<exists>[]\<close>\<close>\<exists>_[_]./ _)\<close> 10)
 syntax_consts
   "_rall" \<rightleftharpoons> rall and
   "_rex" \<rightleftharpoons> rex
diff -r 01b8c8d17f13 -r 2a77bc3b4eac src/ZF/Order.thy
--- a/src/ZF/Order.thy	Fri Sep 20 23:36:33 2024 +0200
+++ b/src/ZF/Order.thy	Fri Sep 20 23:37:00 2024 +0200
@@ -49,7 +49,7 @@
               {f \<in> A->B. \<forall>x\<in>A. \<forall>y\<in>A. \<langle>x,y\<rangle>:r \<longrightarrow> <f`x,f`y>:s}"
 
 definition
-  ord_iso  :: "[i,i,i,i]\<Rightarrow>i"  (\<open>(\<langle>_, _\<rangle> \<cong>/ \<langle>_, _\<rangle>)\<close> 51)  (*Order isomorphisms*)  where
+  ord_iso  :: "[i,i,i,i]\<Rightarrow>i"  (\<open>(\<open>notation=\<open>infix ord_iso\<close>\<close>\<langle>_, _\<rangle> \<cong>/ \<langle>_, _\<rangle>)\<close> 51)  (*Order isomorphisms*)  where
    "\<langle>A,r\<rangle> \<cong> \<langle>B,s\<rangle> \<equiv>
               {f \<in> bij(A,B). \<forall>x\<in>A. \<forall>y\<in>A. \<langle>x,y\<rangle>:r \<longleftrightarrow> <f`x,f`y>:s}"
 
diff -r 01b8c8d17f13 -r 2a77bc3b4eac src/ZF/QPair.thy
--- a/src/ZF/QPair.thy	Fri Sep 20 23:36:33 2024 +0200
+++ b/src/ZF/QPair.thy	Fri Sep 20 23:37:00 2024 +0200
@@ -45,7 +45,7 @@
     "QSigma(A,B)  \<equiv>  \<Union>x\<in>A. \<Union>y\<in>B(x). {<x;y>}"
 
 syntax
-  "_QSUM"   :: "[idt, i, i] \<Rightarrow> i"               (\<open>(3QSUM _ \<in> _./ _)\<close> 10)
+  "_QSUM"   :: "[idt, i, i] \<Rightarrow> i"  (\<open>(\<open>indent=3 notation=\<open>binder QSUM\<in>\<close>\<close>QSUM _ \<in> _./ _)\<close> 10)
 syntax_consts
   "_QSUM" \<rightleftharpoons> QSigma
 translations
diff -r 01b8c8d17f13 -r 2a77bc3b4eac src/ZF/Trancl.thy
--- a/src/ZF/Trancl.thy	Fri Sep 20 23:36:33 2024 +0200
+++ b/src/ZF/Trancl.thy	Fri Sep 20 23:37:00 2024 +0200
@@ -37,11 +37,11 @@
                           \<langle>x,y\<rangle>: r \<longrightarrow> \<langle>y,z\<rangle>: r \<longrightarrow> \<langle>x,z\<rangle>: r"
 
 definition
-  rtrancl :: "i\<Rightarrow>i"  (\<open>(_^*)\<close> [100] 100)  (*refl/transitive closure*)  where
+  rtrancl :: "i\<Rightarrow>i"  (\<open>(\<open>notation=\<open>postfix ^*\<close>\<close>_^*)\<close> [100] 100)  (*refl/transitive closure*)  where
     "r^* \<equiv> lfp(field(r)*field(r), \<lambda>s. id(field(r)) \<union> (r O s))"
 
 definition
-  trancl  :: "i\<Rightarrow>i"  (\<open>(_^+)\<close> [100] 100)  (*transitive closure*)  where
+  trancl  :: "i\<Rightarrow>i"  (\<open>(\<open>notation=\<open>postfix ^+\<close>\<close>_^+)\<close> [100] 100)  (*transitive closure*)  where
     "r^+ \<equiv> r O r^*"
 
 definition
diff -r 01b8c8d17f13 -r 2a77bc3b4eac src/ZF/UNITY/Follows.thy
--- a/src/ZF/UNITY/Follows.thy	Fri Sep 20 23:36:33 2024 +0200
+++ b/src/ZF/UNITY/Follows.thy	Fri Sep 20 23:37:00 2024 +0200
@@ -39,7 +39,7 @@
 
 abbreviation
   Follows' :: "[i\<Rightarrow>i, i\<Rightarrow>i, i, i] \<Rightarrow> i"
-        (\<open>(_ /Fols _ /Wrt (_ /'/ _))\<close> [60, 0, 0, 60] 60)  where
+        (\<open>(\<open>notation=\<open>mixfix Fols Wrt\<close>\<close>_ /Fols _ /Wrt (_ /'/ _))\<close> [60, 0, 0, 60] 60)  where
   "f Fols g Wrt r/A \<equiv> Follows(A,r,f,g)"
 
 
diff -r 01b8c8d17f13 -r 2a77bc3b4eac src/ZF/UNITY/Guar.thy
--- a/src/ZF/UNITY/Guar.thy	Fri Sep 20 23:36:33 2024 +0200
+++ b/src/ZF/UNITY/Guar.thy	Fri Sep 20 23:37:00 2024 +0200
@@ -77,13 +77,13 @@
   "welldef \<equiv> {F \<in> program. Init(F) \<noteq> 0}"
   
 definition
-  refines :: "[i, i, i] \<Rightarrow> o" (\<open>(3_ refines _ wrt _)\<close> [10,10,10] 10)  where
+  refines :: "[i, i, i] \<Rightarrow> o" (\<open>(\<open>indent=3 notation=\<open>mixfix refines wrt\<close>\<close>_ refines _ wrt _)\<close> [10,10,10] 10)  where
   "G refines F wrt X \<equiv>
    \<forall>H \<in> program. (F ok H  \<and> G ok H \<and> F \<squnion> H \<in> welldef \<inter> X)
     \<longrightarrow> (G \<squnion> H \<in> welldef \<inter> X)"
 
 definition
-  iso_refines :: "[i,i, i] \<Rightarrow> o"  (\<open>(3_ iso'_refines _ wrt _)\<close> [10,10,10] 10)  where
+  iso_refines :: "[i,i, i] \<Rightarrow> o"  (\<open>(\<open>indent=3 notation=\<open>mixfix iso_refines wrt\<close>\<close>_ iso'_refines _ wrt _)\<close> [10,10,10] 10)  where
   "G iso_refines F wrt X \<equiv>  F \<in> welldef \<inter> X \<longrightarrow> G \<in> welldef \<inter> X"
 
 
diff -r 01b8c8d17f13 -r 2a77bc3b4eac src/ZF/UNITY/Increasing.thy
--- a/src/ZF/UNITY/Increasing.thy	Fri Sep 20 23:36:33 2024 +0200
+++ b/src/ZF/UNITY/Increasing.thy	Fri Sep 20 23:37:00 2024 +0200
@@ -23,7 +23,7 @@
                 (\<forall>x \<in> state. f(x):A)}"
 
 abbreviation (input)
-  IncWrt ::  "[i\<Rightarrow>i, i, i] \<Rightarrow> i" (\<open>(_ IncreasingWrt _ '/ _)\<close> [60, 0, 60] 60)  where
+  IncWrt ::  "[i\<Rightarrow>i, i, i] \<Rightarrow> i" (\<open>(\<open>notation=\<open>mixfix IncreasingWrt\<close>\<close>_ IncreasingWrt _ '/ _)\<close> [60, 0, 60] 60)  where
   "f IncreasingWrt r/A \<equiv> Increasing[A](r,f)"
 
 
diff -r 01b8c8d17f13 -r 2a77bc3b4eac src/ZF/UNITY/Union.thy
--- a/src/ZF/UNITY/Union.thy	Fri Sep 20 23:36:33 2024 +0200
+++ b/src/ZF/UNITY/Union.thy	Fri Sep 20 23:37:00 2024 +0200
@@ -41,8 +41,8 @@
       SKIP \<in> X \<and> (\<forall>G \<in> program. Acts(G) \<subseteq> (\<Union>F \<in> X. Acts(F)) \<longrightarrow> G \<in> X)"
 
 syntax
-  "_JOIN1"  :: "[pttrns, i] \<Rightarrow> i"     (\<open>(3\<Squnion>_./ _)\<close> 10)
-  "_JOIN"   :: "[pttrn, i, i] \<Rightarrow> i"   (\<open>(3\<Squnion>_ \<in> _./ _)\<close> 10)
+  "_JOIN1"  :: "[pttrns, i] \<Rightarrow> i"     (\<open>(\<open>indent=3 notation=\<open>binder \<Squnion>\<close>\<close>\<Squnion>_./ _)\<close> 10)
+  "_JOIN"   :: "[pttrn, i, i] \<Rightarrow> i"   (\<open>(\<open>indent=3 notation=\<open>binder \<Squnion>\<in>\<close>\<close>\<Squnion>_ \<in> _./ _)\<close> 10)
 syntax_consts
   "_JOIN1" "_JOIN" == JOIN
 translations
diff -r 01b8c8d17f13 -r 2a77bc3b4eac src/ZF/ZF.thy
--- a/src/ZF/ZF.thy	Fri Sep 20 23:36:33 2024 +0200
+++ b/src/ZF/ZF.thy	Fri Sep 20 23:37:00 2024 +0200
@@ -7,14 +7,14 @@
 
 subsection\<open>Iteration of the function \<^term>\<open>F\<close>\<close>
 
-consts  iterates :: "[i\<Rightarrow>i,i,i] \<Rightarrow> i"   (\<open>(_^_ '(_'))\<close> [60,1000,1000] 60)
+consts  iterates :: "[i\<Rightarrow>i,i,i] \<Rightarrow> i"  (\<open>(\<open>notation=\<open>mixfix iterates\<close>\<close>_^_ '(_'))\<close> [60,1000,1000] 60)
 
 primrec
     "F^0 (x) = x"
     "F^(succ(n)) (x) = F(F^n (x))"
 
 definition
-  iterates_omega :: "[i\<Rightarrow>i,i] \<Rightarrow> i" (\<open>(_^\<omega> '(_'))\<close> [60,1000] 60) where
+  iterates_omega :: "[i\<Rightarrow>i,i] \<Rightarrow> i" (\<open>(\<open>notation=\<open>mixfix iterates_omega\<close>\<close>_^\<omega> '(_'))\<close> [60,1000] 60) where
     "F^\<omega> (x) \<equiv> \<Union>n\<in>nat. F^n (x)"
 
 lemma iterates_triv:
diff -r 01b8c8d17f13 -r 2a77bc3b4eac src/ZF/ZF_Base.thy
--- a/src/ZF/ZF_Base.thy	Fri Sep 20 23:36:33 2024 +0200
+++ b/src/ZF/ZF_Base.thy	Fri Sep 20 23:37:00 2024 +0200
@@ -36,8 +36,8 @@
   where "Bex(A, P) \<equiv> \<exists>x. x\<in>A \<and> P(x)"
 
 syntax
-  "_Ball" :: "[pttrn, i, o] \<Rightarrow> o"  (\<open>(3\<forall>_\<in>_./ _)\<close> 10)
-  "_Bex" :: "[pttrn, i, o] \<Rightarrow> o"  (\<open>(3\<exists>_\<in>_./ _)\<close> 10)
+  "_Ball" :: "[pttrn, i, o] \<Rightarrow> o"  (\<open>(\<open>indent=3 notation=\<open>binder \<forall>\<in>\<close>\<close>\<forall>_\<in>_./ _)\<close> 10)
+  "_Bex" :: "[pttrn, i, o] \<Rightarrow> o"  (\<open>(\<open>indent=3 notation=\<open>binder \<exists>\<in>\<close>\<close>\<exists>_\<in>_./ _)\<close> 10)
 syntax_consts
   "_Ball" \<rightleftharpoons> Ball and
   "_Bex" \<rightleftharpoons> Bex
@@ -55,7 +55,7 @@
   where "Replace(A,P) \<equiv> PrimReplace(A, \<lambda>x y. (\<exists>!z. P(x,z)) \<and> P(x,y))"
 
 syntax
-  "_Replace" :: "[pttrn, pttrn, i, o] \<Rightarrow> i"  (\<open>(1{_ ./ _ \<in> _, _})\<close>)
+  "_Replace" :: "[pttrn, pttrn, i, o] \<Rightarrow> i"  (\<open>(\<open>indent=1 notation=\<open>mixfix Replace\<close>\<close>{_ ./ _ \<in> _, _})\<close>)
 syntax_consts
   "_Replace" \<rightleftharpoons> Replace
 translations
@@ -68,7 +68,7 @@
   where "RepFun(A,f) \<equiv> {y . x\<in>A, y=f(x)}"
 
 syntax
-  "_RepFun" :: "[i, pttrn, i] \<Rightarrow> i"  (\<open>(1{_ ./ _ \<in> _})\<close> [51,0,51])
+  "_RepFun" :: "[i, pttrn, i] \<Rightarrow> i"  (\<open>(\<open>indent=1 notation=\<open>mixfix RepFun\<close>\<close>{_ ./ _ \<in> _})\<close> [51,0,51])
 syntax_consts
   "_RepFun" \<rightleftharpoons> RepFun
 translations
@@ -80,7 +80,7 @@
   where "Collect(A,P) \<equiv> {y . x\<in>A, x=y \<and> P(x)}"
 
 syntax
-  "_Collect" :: "[pttrn, i, o] \<Rightarrow> i"  (\<open>(1{_ \<in> _ ./ _})\<close>)
+  "_Collect" :: "[pttrn, i, o] \<Rightarrow> i"  (\<open>(\<open>indent=1 notation=\<open>mixfix Collect\<close>\<close>{_ \<in> _ ./ _})\<close>)
 syntax_consts
   "_Collect" \<rightleftharpoons> Collect
 translations
@@ -93,8 +93,8 @@
   where "\<Inter>(A) \<equiv> { x\<in>\<Union>(A) . \<forall>y\<in>A. x\<in>y}"
 
 syntax
-  "_UNION" :: "[pttrn, i, i] \<Rightarrow> i"  (\<open>(3\<Union>_\<in>_./ _)\<close> 10)
-  "_INTER" :: "[pttrn, i, i] \<Rightarrow> i"  (\<open>(3\<Inter>_\<in>_./ _)\<close> 10)
+  "_UNION" :: "[pttrn, i, i] \<Rightarrow> i"  (\<open>(\<open>indent=3 notation=\<open>binder \<Union>\<in>\<close>\<close>\<Union>_\<in>_./ _)\<close> 10)
+  "_INTER" :: "[pttrn, i, i] \<Rightarrow> i"  (\<open>(\<open>indent=3 notation=\<open>binder \<Inter>\<in>\<close>\<close>\<Inter>_\<in>_./ _)\<close> 10)
 syntax_consts
   "_UNION" == Union and
   "_INTER" == Inter
@@ -169,7 +169,7 @@
 definition The :: "(i \<Rightarrow> o) \<Rightarrow> i"  (binder \<open>THE \<close> 10)
   where the_def: "The(P)    \<equiv> \<Union>({y . x \<in> {0}, P(y)})"
 
-definition If :: "[o, i, i] \<Rightarrow> i"  (\<open>(if (_)/ then (_)/ else (_))\<close> [10] 10)
+definition If :: "[o, i, i] \<Rightarrow> i"  (\<open>(\<open>notation=\<open>mixfix if then else\<close>\<close>if (_)/ then (_)/ else (_))\<close> [10] 10)
   where if_def: "if P then a else b \<equiv> THE z. P \<and> z=a | \<not>P \<and> z=b"
 
 abbreviation (input)
@@ -272,9 +272,9 @@
 (* binder syntax *)
 
 syntax
-  "_PROD"     :: "[pttrn, i, i] \<Rightarrow> i"        (\<open>(3\<Prod>_\<in>_./ _)\<close> 10)
-  "_SUM"      :: "[pttrn, i, i] \<Rightarrow> i"        (\<open>(3\<Sum>_\<in>_./ _)\<close> 10)
-  "_lam"      :: "[pttrn, i, i] \<Rightarrow> i"        (\<open>(3\<lambda>_\<in>_./ _)\<close> 10)
+  "_PROD"     :: "[pttrn, i, i] \<Rightarrow> i"        (\<open>(\<open>indent=3 notation=\<open>mixfix \<Prod>\<in>\<close>\<close>\<Prod>_\<in>_./ _)\<close> 10)
+  "_SUM"      :: "[pttrn, i, i] \<Rightarrow> i"        (\<open>(\<open>indent=3 notation=\<open>mixfix \<Sum>\<in>\<close>\<close>\<Sum>_\<in>_./ _)\<close> 10)
+  "_lam"      :: "[pttrn, i, i] \<Rightarrow> i"        (\<open>(\<open>indent=3 notation=\<open>mixfix \<lambda>\<in>\<close>\<close>\<lambda>_\<in>_./ _)\<close> 10)
 syntax_consts
   "_PROD" == Pi and
   "_SUM" == Sigma and
@@ -297,16 +297,16 @@
   not_mem         (infixl \<open>\<not>:\<close> 50)
 
 syntax (ASCII)
-  "_Ball"     :: "[pttrn, i, o] \<Rightarrow> o"        (\<open>(3ALL _:_./ _)\<close> 10)
-  "_Bex"      :: "[pttrn, i, o] \<Rightarrow> o"        (\<open>(3EX _:_./ _)\<close> 10)
-  "_Collect"  :: "[pttrn, i, o] \<Rightarrow> i"        (\<open>(1{_: _ ./ _})\<close>)
-  "_Replace"  :: "[pttrn, pttrn, i, o] \<Rightarrow> i" (\<open>(1{_ ./ _: _, _})\<close>)
-  "_RepFun"   :: "[i, pttrn, i] \<Rightarrow> i"        (\<open>(1{_ ./ _: _})\<close> [51,0,51])
-  "_UNION"    :: "[pttrn, i, i] \<Rightarrow> i"        (\<open>(3UN _:_./ _)\<close> 10)
-  "_INTER"    :: "[pttrn, i, i] \<Rightarrow> i"        (\<open>(3INT _:_./ _)\<close> 10)
-  "_PROD"     :: "[pttrn, i, i] \<Rightarrow> i"        (\<open>(3PROD _:_./ _)\<close> 10)
-  "_SUM"      :: "[pttrn, i, i] \<Rightarrow> i"        (\<open>(3SUM _:_./ _)\<close> 10)
-  "_lam"      :: "[pttrn, i, i] \<Rightarrow> i"        (\<open>(3lam _:_./ _)\<close> 10)
+  "_Ball"     :: "[pttrn, i, o] \<Rightarrow> o"        (\<open>(\<open>indent=3 notation=\<open>binder ALL:\<close>\<close>ALL _:_./ _)\<close> 10)
+  "_Bex"      :: "[pttrn, i, o] \<Rightarrow> o"        (\<open>(\<open>indent=3 notation=\<open>binder EX:\<close>\<close>EX _:_./ _)\<close> 10)
+  "_Collect"  :: "[pttrn, i, o] \<Rightarrow> i"        (\<open>(\<open>indent=1 notation=\<open>mixfix Collect\<close>\<close>{_: _ ./ _})\<close>)
+  "_Replace"  :: "[pttrn, pttrn, i, o] \<Rightarrow> i" (\<open>(\<open>indent=1 notation=\<open>mixfix Replace\<close>\<close>{_ ./ _: _, _})\<close>)
+  "_RepFun"   :: "[i, pttrn, i] \<Rightarrow> i"        (\<open>(\<open>indent=1 notation=\<open>mixfix RepFun\<close>\<close>{_ ./ _: _})\<close> [51,0,51])
+  "_UNION"    :: "[pttrn, i, i] \<Rightarrow> i"        (\<open>(\<open>indent=3 notation=\<open>binder UN:\<close>\<close>UN _:_./ _)\<close> 10)
+  "_INTER"    :: "[pttrn, i, i] \<Rightarrow> i"        (\<open>(\<open>indent=3 notation=\<open>binder INT:\<close>\<close>INT _:_./ _)\<close> 10)
+  "_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>)
   "_pattern"  :: "patterns \<Rightarrow> pttrn"         (\<open><_>\<close>)
 
diff -r 01b8c8d17f13 -r 2a77bc3b4eac src/ZF/ex/Ring.thy
--- a/src/ZF/ex/Ring.thy	Fri Sep 20 23:36:33 2024 +0200
+++ b/src/ZF/ex/Ring.thy	Fri Sep 20 23:37:00 2024 +0200
@@ -46,7 +46,7 @@
   "a_inv(R) \<equiv> m_inv (<carrier(R), add_field(R), zero(R), 0>)"
 
 definition
-  minus :: "[i,i,i] \<Rightarrow> i" (\<open>(_ \<ominus>\<index> _)\<close> [65,66] 65) where
+  minus :: "[i,i,i] \<Rightarrow> i" (\<open>(\<open>notation=\<open>infix \<ominus>\<close>\<close>_ \<ominus>\<index> _)\<close> [65,66] 65) where
   "\<lbrakk>x \<in> carrier(R); y \<in> carrier(R)\<rbrakk> \<Longrightarrow> x \<ominus>\<^bsub>R\<^esub> y = x \<oplus>\<^bsub>R\<^esub> (\<ominus>\<^bsub>R\<^esub> y)"
 
 locale abelian_monoid = fixes G (structure)
diff -r 01b8c8d17f13 -r 2a77bc3b4eac src/ZF/func.thy
--- a/src/ZF/func.thy	Fri Sep 20 23:36:33 2024 +0200
+++ b/src/ZF/func.thy	Fri Sep 20 23:37:00 2024 +0200
@@ -448,7 +448,7 @@
 nonterminal updbinds and updbind
 
 syntax
-  "_updbind"    :: "[i, i] \<Rightarrow> updbind"               (\<open>(2_ :=/ _)\<close>)
+  "_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)