# HG changeset patch
# User wenzelm
# Date 1727818570 -7200
# Node ID 49c04500c5f90154d6204ee356b9a185e7b37281
# Parent  2a8afc91ce9c5b4e235091256c8e125fd8bddbd8
more inner syntax markup: HOLCF;

diff -r 2a8afc91ce9c -r 49c04500c5f9 src/HOL/HOLCF/Cfun.thy
--- a/src/HOL/HOLCF/Cfun.thy	Tue Oct 01 22:12:11 2024 +0200
+++ b/src/HOL/HOLCF/Cfun.thy	Tue Oct 01 23:36:10 2024 +0200
@@ -16,17 +16,17 @@
 
 definition "cfun = {f::'a \<Rightarrow> 'b. cont f}"
 
-cpodef ('a, 'b) cfun (\<open>(_ \<rightarrow>/ _)\<close> [1, 0] 0) = "cfun :: ('a \<Rightarrow> 'b) set"
+cpodef ('a, 'b) cfun (\<open>(\<open>notation=\<open>infix \<rightarrow>\<close>\<close>_ \<rightarrow>/ _)\<close> [1, 0] 0) = "cfun :: ('a \<Rightarrow> 'b) set"
   by (auto simp: cfun_def intro: cont_const adm_cont)
 
 type_notation (ASCII)
   cfun  (infixr \<open>->\<close> 0)
 
 notation (ASCII)
-  Rep_cfun  (\<open>(_$/_)\<close> [999,1000] 999)
+  Rep_cfun  (\<open>(\<open>notation=\<open>infix $\<close>\<close>_$/_)\<close> [999,1000] 999)
 
 notation
-  Rep_cfun  (\<open>(_\<cdot>/_)\<close> [999,1000] 999)
+  Rep_cfun  (\<open>(\<open>notation=\<open>infix \<cdot>\<close>\<close>_\<cdot>/_)\<close> [999,1000] 999)
 
 
 subsection \<open>Syntax for continuous lambda abstraction\<close>
@@ -47,10 +47,10 @@
 text \<open>Syntax for nested abstractions\<close>
 
 syntax (ASCII)
-  "_Lambda" :: "[cargs, logic] \<Rightarrow> logic"  (\<open>(3LAM _./ _)\<close> [1000, 10] 10)
+  "_Lambda" :: "[cargs, logic] \<Rightarrow> logic"  (\<open>(\<open>indent=3 notation=\<open>binder LAM\<close>\<close>LAM _./ _)\<close> [1000, 10] 10)
 
 syntax
-  "_Lambda" :: "[cargs, logic] \<Rightarrow> logic" (\<open>(3\<Lambda> _./ _)\<close> [1000, 10] 10)
+  "_Lambda" :: "[cargs, logic] \<Rightarrow> logic" (\<open>(\<open>indent=3 notation=\<open>binder \<Lambda>\<close>\<close>\<Lambda> _./ _)\<close> [1000, 10] 10)
 
 syntax_consts
   "_Lambda" \<rightleftharpoons> Abs_cfun
diff -r 2a8afc91ce9c -r 49c04500c5f9 src/HOL/HOLCF/ConvexPD.thy
--- a/src/HOL/HOLCF/ConvexPD.thy	Tue Oct 01 22:12:11 2024 +0200
+++ b/src/HOL/HOLCF/ConvexPD.thy	Tue Oct 01 23:36:10 2024 +0200
@@ -119,7 +119,7 @@
 
 subsection \<open>Type definition\<close>
 
-typedef 'a convex_pd  (\<open>('(_')\<natural>)\<close>) =
+typedef 'a convex_pd  (\<open>(\<open>notation=\<open>postfix convex_pd\<close>\<close>'(_')\<natural>)\<close>) =
   "{S::'a pd_basis set. convex_le.ideal S}"
 by (rule convex_le.ex_ideal)
 
@@ -345,10 +345,7 @@
 
 syntax
   "_convex_bind" :: "[logic, logic, logic] \<Rightarrow> logic"
-    (\<open>(3\<Union>\<natural>_\<in>_./ _)\<close> [0, 0, 10] 10)
-
-syntax_consts
-  "_convex_bind" == convex_bind
+    (\<open>(\<open>indent=3 notation=\<open>binder convex_bind\<close>\<close>\<Union>\<natural>_\<in>_./ _)\<close> [0, 0, 10] 10)
 
 translations
   "\<Union>\<natural>x\<in>xs. e" == "CONST convex_bind\<cdot>xs\<cdot>(\<Lambda> x. e)"
diff -r 2a8afc91ce9c -r 49c04500c5f9 src/HOL/HOLCF/FOCUS/Fstream.thy
--- a/src/HOL/HOLCF/FOCUS/Fstream.thy	Tue Oct 01 22:12:11 2024 +0200
+++ b/src/HOL/HOLCF/FOCUS/Fstream.thy	Tue Oct 01 23:36:10 2024 +0200
@@ -29,16 +29,16 @@
   "<> == \<bottom>"
 
 abbreviation
-  fscons'       :: "'a \<Rightarrow> 'a fstream \<Rightarrow> 'a fstream"       (\<open>(_\<leadsto>_)\<close> [66,65] 65) where
+  fscons'       :: "'a \<Rightarrow> 'a fstream \<Rightarrow> 'a fstream"       (\<open>(\<open>notation=\<open>infix \<leadsto>\<close>\<close>_\<leadsto>_)\<close> [66,65] 65) where
   "a\<leadsto>s == fscons a\<cdot>s"
 
 abbreviation
-  fsfilter'     :: "'a set \<Rightarrow> 'a fstream \<Rightarrow> 'a fstream"   (\<open>(_\<copyright>_)\<close> [64,63] 63) where
+  fsfilter'     :: "'a set \<Rightarrow> 'a fstream \<Rightarrow> 'a fstream"   (\<open>(\<open>notation=\<open>infix \<copyright>\<close>\<close>_\<copyright>_)\<close> [64,63] 63) where
   "A\<copyright>s == fsfilter A\<cdot>s"
 
 notation (ASCII)
-  fscons'  (\<open>(_~>_)\<close> [66,65] 65) and
-  fsfilter'  (\<open>(_'(C')_)\<close> [64,63] 63)
+  fscons'  (\<open>(\<open>notation=\<open>infix ~>\<close>\<close>_~>_)\<close> [66,65] 65) and
+  fsfilter'  (\<open>(\<open>notation=\<open>infix (C)\<close>\<close>_'(C')_)\<close> [64,63] 63)
 
 
 lemma Def_maximal: "a = Def d \<Longrightarrow> a\<sqsubseteq>b \<Longrightarrow> b = Def d"
diff -r 2a8afc91ce9c -r 49c04500c5f9 src/HOL/HOLCF/FOCUS/Fstreams.thy
--- a/src/HOL/HOLCF/FOCUS/Fstreams.thy	Tue Oct 01 22:12:11 2024 +0200
+++ b/src/HOL/HOLCF/FOCUS/Fstreams.thy	Tue Oct 01 23:36:10 2024 +0200
@@ -44,11 +44,11 @@
   "<> == \<bottom>"
 
 abbreviation
-  fsfilter' :: "'a set \<Rightarrow> 'a fstream \<Rightarrow> 'a fstream"       (\<open>(_\<copyright>_)\<close> [64,63] 63) where
+  fsfilter' :: "'a set \<Rightarrow> 'a fstream \<Rightarrow> 'a fstream"       (\<open>(\<open>notation=\<open>infix \<copyright>\<close>\<close>_\<copyright>_)\<close> [64,63] 63) where
   "A\<copyright>s == fsfilter A\<cdot>s"
 
 notation (ASCII)
-  fsfilter'  (\<open>(_'(C')_)\<close> [64,63] 63)
+  fsfilter'  (\<open>(\<open>notation=\<open>infix (C)\<close>\<close>_'(C')_)\<close> [64,63] 63)
 
 
 lemma ft_fsingleton[simp]: "ft\<cdot>(<a>) = Def a"
diff -r 2a8afc91ce9c -r 49c04500c5f9 src/HOL/HOLCF/IOA/Sequence.thy
--- a/src/HOL/HOLCF/IOA/Sequence.thy	Tue Oct 01 22:12:11 2024 +0200
+++ b/src/HOL/HOLCF/IOA/Sequence.thy	Tue Oct 01 23:36:10 2024 +0200
@@ -63,7 +63,7 @@
               UU \<Rightarrow> UU
             | Def y \<Rightarrow> (if P y then x ## (h \<cdot> xs) else h \<cdot> xs))))"
 
-abbreviation Consq_syn  (\<open>(_/\<leadsto>_)\<close> [66, 65] 65)
+abbreviation Consq_syn  (\<open>(\<open>notation=\<open>infix \<leadsto>\<close>\<close>_/\<leadsto>_)\<close> [66, 65] 65)
   where "a \<leadsto> s \<equiv> Consq a \<cdot> s"
 
 
diff -r 2a8afc91ce9c -r 49c04500c5f9 src/HOL/HOLCF/IOA/TL.thy
--- a/src/HOL/HOLCF/IOA/TL.thy	Tue Oct 01 22:12:11 2024 +0200
+++ b/src/HOL/HOLCF/IOA/TL.thy	Tue Oct 01 23:36:10 2024 +0200
@@ -22,7 +22,7 @@
   where "Init P s = P (unlift (HD \<cdot> s))"
     \<comment> \<open>this means that for \<open>nil\<close> and \<open>UU\<close> the effect is unpredictable\<close>
 
-definition Next :: "'a temporal \<Rightarrow> 'a temporal"  (\<open>\<circle>(_)\<close> [80] 80)
+definition Next :: "'a temporal \<Rightarrow> 'a temporal"  (\<open>(\<open>indent=1 notation=\<open>prefix Next\<close>\<close>\<circle>_)\<close> [80] 80)
   where "(\<circle>P) s \<longleftrightarrow> (if TL \<cdot> s = UU \<or> TL \<cdot> s = nil then P s else P (TL \<cdot> s))"
 
 definition suffix :: "'a Seq \<Rightarrow> 'a Seq \<Rightarrow> bool"
@@ -31,10 +31,10 @@
 definition tsuffix :: "'a Seq \<Rightarrow> 'a Seq \<Rightarrow> bool"
   where "tsuffix s2 s \<longleftrightarrow> s2 \<noteq> nil \<and> s2 \<noteq> UU \<and> suffix s2 s"
 
-definition Box :: "'a temporal \<Rightarrow> 'a temporal"  (\<open>\<box>(_)\<close> [80] 80)
+definition Box :: "'a temporal \<Rightarrow> 'a temporal"  (\<open>(\<open>indent=1 notation=\<open>prefix Box\<close>\<close>\<box>_)\<close> [80] 80)
   where "(\<box>P) s \<longleftrightarrow> (\<forall>s2. tsuffix s2 s \<longrightarrow> P s2)"
 
-definition Diamond :: "'a temporal \<Rightarrow> 'a temporal"  (\<open>\<diamond>(_)\<close> [80] 80)
+definition Diamond :: "'a temporal \<Rightarrow> 'a temporal"  (\<open>(\<open>indent=1 notation=\<open>prefix Diamond\<close>\<close>\<diamond>_)\<close> [80] 80)
   where "\<diamond>P = (\<^bold>\<not> (\<box>(\<^bold>\<not> P)))"
 
 definition Leadsto :: "'a temporal \<Rightarrow> 'a temporal \<Rightarrow> 'a temporal"  (infixr \<open>\<leadsto>\<close> 22)
diff -r 2a8afc91ce9c -r 49c04500c5f9 src/HOL/HOLCF/LowerPD.thy
--- a/src/HOL/HOLCF/LowerPD.thy	Tue Oct 01 22:12:11 2024 +0200
+++ b/src/HOL/HOLCF/LowerPD.thy	Tue Oct 01 23:36:10 2024 +0200
@@ -74,7 +74,7 @@
 
 subsection \<open>Type definition\<close>
 
-typedef 'a lower_pd  (\<open>('(_')\<flat>)\<close>) =
+typedef 'a lower_pd  (\<open>(\<open>notation=\<open>postfix lower_pd\<close>\<close>'(_')\<flat>)\<close>) =
   "{S::'a pd_basis set. lower_le.ideal S}"
 by (rule lower_le.ex_ideal)
 
@@ -339,10 +339,7 @@
 
 syntax
   "_lower_bind" :: "[logic, logic, logic] \<Rightarrow> logic"
-    (\<open>(3\<Union>\<flat>_\<in>_./ _)\<close> [0, 0, 10] 10)
-
-syntax_consts
-  "_lower_bind" == lower_bind
+    (\<open>(\<open>indent=3 notation=\<open>binder lower_bind\<close>\<close>\<Union>\<flat>_\<in>_./ _)\<close> [0, 0, 10] 10)
 
 translations
   "\<Union>\<flat>x\<in>xs. e" == "CONST lower_bind\<cdot>xs\<cdot>(\<Lambda> x. e)"
diff -r 2a8afc91ce9c -r 49c04500c5f9 src/HOL/HOLCF/Porder.thy
--- a/src/HOL/HOLCF/Porder.thy	Tue Oct 01 22:12:11 2024 +0200
+++ b/src/HOL/HOLCF/Porder.thy	Tue Oct 01 23:36:10 2024 +0200
@@ -113,10 +113,10 @@
 end
 
 syntax (ASCII)
-  "_BLub" :: "[pttrn, 'a set, 'b] \<Rightarrow> 'b" (\<open>(3LUB _:_./ _)\<close> [0,0, 10] 10)
+  "_BLub" :: "[pttrn, 'a set, 'b] \<Rightarrow> 'b" (\<open>(\<open>indent=3 notation=\<open>binder LUB\<close>\<close>LUB _:_./ _)\<close> [0,0, 10] 10)
 
 syntax
-  "_BLub" :: "[pttrn, 'a set, 'b] \<Rightarrow> 'b" (\<open>(3\<Squnion>_\<in>_./ _)\<close> [0,0, 10] 10)
+  "_BLub" :: "[pttrn, 'a set, 'b] \<Rightarrow> 'b" (\<open>(\<open>indent=3 notation=\<open>binder \<Squnion>\<close>\<close>\<Squnion>_\<in>_./ _)\<close> [0,0, 10] 10)
 
 syntax_consts
   "_BLub" \<rightleftharpoons> lub
diff -r 2a8afc91ce9c -r 49c04500c5f9 src/HOL/HOLCF/Sprod.thy
--- a/src/HOL/HOLCF/Sprod.thy	Tue Oct 01 22:12:11 2024 +0200
+++ b/src/HOL/HOLCF/Sprod.thy	Tue Oct 01 23:36:10 2024 +0200
@@ -16,7 +16,7 @@
 
 definition "sprod = {p::'a \<times> 'b. p = \<bottom> \<or> (fst p \<noteq> \<bottom> \<and> snd p \<noteq> \<bottom>)}"
 
-pcpodef ('a, 'b) sprod  (\<open>(_ \<otimes>/ _)\<close> [21,20] 20) = "sprod :: ('a \<times> 'b) set"
+pcpodef ('a, 'b) sprod  (\<open>(\<open>notation=\<open>infix strict product\<close>\<close>_ \<otimes>/ _)\<close> [21,20] 20) = "sprod :: ('a \<times> 'b) set"
   by (simp_all add: sprod_def)
 
 instance sprod :: ("{chfin,pcpo}", "{chfin,pcpo}") chfin
diff -r 2a8afc91ce9c -r 49c04500c5f9 src/HOL/HOLCF/Ssum.thy
--- a/src/HOL/HOLCF/Ssum.thy	Tue Oct 01 22:12:11 2024 +0200
+++ b/src/HOL/HOLCF/Ssum.thy	Tue Oct 01 23:36:10 2024 +0200
@@ -19,7 +19,7 @@
     (fst p = TT \<and> fst (snd p) \<noteq> \<bottom> \<and> snd (snd p) = \<bottom>) \<or>
     (fst p = FF \<and> fst (snd p) = \<bottom> \<and> snd (snd p) \<noteq> \<bottom>)}"
 
-pcpodef ('a, 'b) ssum  (\<open>(_ \<oplus>/ _)\<close> [21, 20] 20) = "ssum :: (tr \<times> 'a \<times> 'b) set"
+pcpodef ('a, 'b) ssum  (\<open>(\<open>notation=\<open>infix strict sum\<close>\<close>_ \<oplus>/ _)\<close> [21, 20] 20) = "ssum :: (tr \<times> 'a \<times> 'b) set"
   by (simp_all add: ssum_def)
 
 instance ssum :: ("{chfin,pcpo}", "{chfin,pcpo}") chfin
diff -r 2a8afc91ce9c -r 49c04500c5f9 src/HOL/HOLCF/Tr.thy
--- a/src/HOL/HOLCF/Tr.thy	Tue Oct 01 22:12:11 2024 +0200
+++ b/src/HOL/HOLCF/Tr.thy	Tue Oct 01 23:36:10 2024 +0200
@@ -63,7 +63,7 @@
 definition tr_case :: "'a \<rightarrow> 'a \<rightarrow> tr \<rightarrow> 'a"
   where "tr_case = (\<Lambda> t e (Def b). if b then t else e)"
 
-abbreviation cifte_syn :: "[tr, 'c, 'c] \<Rightarrow> 'c"  (\<open>(If (_)/ then (_)/ else (_))\<close> [0, 0, 60] 60)
+abbreviation cifte_syn :: "[tr, 'c, 'c] \<Rightarrow> 'c"  (\<open>(\<open>notation=\<open>mixfix If expression\<close>\<close>If (_)/ then (_)/ else (_))\<close> [0, 0, 60] 60)
   where "If b then e1 else e2 \<equiv> tr_case\<cdot>e1\<cdot>e2\<cdot>b"
 
 translations
diff -r 2a8afc91ce9c -r 49c04500c5f9 src/HOL/HOLCF/Up.thy
--- a/src/HOL/HOLCF/Up.thy	Tue Oct 01 22:12:11 2024 +0200
+++ b/src/HOL/HOLCF/Up.thy	Tue Oct 01 23:36:10 2024 +0200
@@ -14,7 +14,7 @@
 
 subsection \<open>Definition of new type for lifting\<close>
 
-datatype 'a u  (\<open>(_\<^sub>\<bottom>)\<close> [1000] 999) = Ibottom | Iup 'a
+datatype 'a u  (\<open>(\<open>notation=\<open>postfix lifting\<close>\<close>_\<^sub>\<bottom>)\<close> [1000] 999) = Ibottom | Iup 'a
 
 primrec Ifup :: "('a \<rightarrow> 'b::pcpo) \<Rightarrow> 'a u \<Rightarrow> 'b"
   where
diff -r 2a8afc91ce9c -r 49c04500c5f9 src/HOL/HOLCF/UpperPD.thy
--- a/src/HOL/HOLCF/UpperPD.thy	Tue Oct 01 22:12:11 2024 +0200
+++ b/src/HOL/HOLCF/UpperPD.thy	Tue Oct 01 23:36:10 2024 +0200
@@ -72,7 +72,7 @@
 
 subsection \<open>Type definition\<close>
 
-typedef 'a upper_pd  (\<open>('(_')\<sharp>)\<close>) =
+typedef 'a upper_pd  (\<open>(\<open>notation=\<open>postfix upper_pd\<close>\<close>'(_')\<sharp>)\<close>) =
   "{S::'a pd_basis set. upper_le.ideal S}"
 by (rule upper_le.ex_ideal)
 
@@ -332,10 +332,7 @@
 
 syntax
   "_upper_bind" :: "[logic, logic, logic] \<Rightarrow> logic"
-    (\<open>(3\<Union>\<sharp>_\<in>_./ _)\<close> [0, 0, 10] 10)
-
-syntax_consts
-  "_upper_bind" == upper_bind
+    (\<open>(\<open>indent=3 notation=\<open>binder upper_bind\<close>\<close>\<Union>\<sharp>_\<in>_./ _)\<close> [0, 0, 10] 10)
 
 translations
   "\<Union>\<sharp>x\<in>xs. e" == "CONST upper_bind\<cdot>xs\<cdot>(\<Lambda> x. e)"
diff -r 2a8afc91ce9c -r 49c04500c5f9 src/HOL/HOLCF/ex/Letrec.thy
--- a/src/HOL/HOLCF/ex/Letrec.thy	Tue Oct 01 22:12:11 2024 +0200
+++ b/src/HOL/HOLCF/ex/Letrec.thy	Tue Oct 01 23:36:10 2024 +0200
@@ -15,15 +15,12 @@
 nonterminal recbinds and recbindt and recbind
 
 syntax
-  "_recbind"  :: "[logic, logic] \<Rightarrow> recbind"         (\<open>(2_ =/ _)\<close> 10)
+  "_recbind"  :: "[logic, logic] \<Rightarrow> recbind"         (\<open>(\<open>indent=2 notation=\<open>mixfix Letrec binding\<close>\<close>_ =/ _)\<close> 10)
   ""          :: "recbind \<Rightarrow> recbindt"               (\<open>_\<close>)
   "_recbindt" :: "[recbind, recbindt] \<Rightarrow> recbindt"   (\<open>_,/ _\<close>)
   ""          :: "recbindt \<Rightarrow> recbinds"              (\<open>_\<close>)
   "_recbinds" :: "[recbindt, recbinds] \<Rightarrow> recbinds"  (\<open>_;/ _\<close>)
-  "_Letrec"   :: "[recbinds, logic] \<Rightarrow> logic"        (\<open>(Letrec (_)/ in (_))\<close> 10)
-
-syntax_consts
-  "_recbind" "_recbinds" "_recbindt" "_Letrec" == CLetrec
+  "_Letrec"   :: "[recbinds, logic] \<Rightarrow> logic"        (\<open>(\<open>notation=\<open>mixfix Letrec expression\<close>\<close>Letrec (_)/ in (_))\<close> 10)
 
 translations
   (recbindt) "x = a, (y,ys) = (b,bs)" == (recbindt) "(x,y,ys) = (a,b,bs)"
diff -r 2a8afc91ce9c -r 49c04500c5f9 src/HOL/HOLCF/ex/Pattern_Match.thy
--- a/src/HOL/HOLCF/ex/Pattern_Match.thy	Tue Oct 01 22:12:11 2024 +0200
+++ b/src/HOL/HOLCF/ex/Pattern_Match.thy	Tue Oct 01 23:36:10 2024 +0200
@@ -103,14 +103,14 @@
 nonterminal Case_pat and Case_syn and Cases_syn
 
 syntax
-  "_Case_syntax":: "['a, Cases_syn] => 'b"               (\<open>(Case _ of/ _)\<close> 10)
-  "_Case1"      :: "[Case_pat, 'b] => Case_syn"          (\<open>(2_ \<Rightarrow>/ _)\<close> 10)
+  "_Case_syntax":: "['a, Cases_syn] => 'b"               (\<open>(\<open>notation=\<open>mixfix Case expression\<close>\<close>Case _ of/ _)\<close> 10)
+  "_Case1"      :: "[Case_pat, 'b] => Case_syn"          (\<open>(\<open>indent=2 notation=\<open>mixfix Case clause\<close>\<close>_ \<Rightarrow>/ _)\<close> 10)
   ""            :: "Case_syn => Cases_syn"               (\<open>_\<close>)
   "_Case2"      :: "[Case_syn, Cases_syn] => Cases_syn"  (\<open>_/ | _\<close>)
   "_strip_positions" :: "'a => Case_pat"                 (\<open>_\<close>)
 
 syntax (ASCII)
-  "_Case1"      :: "[Case_pat, 'b] => Case_syn"          (\<open>(2_ =>/ _)\<close> 10)
+  "_Case1"      :: "[Case_pat, 'b] => Case_syn"          (\<open>(\<open>indent=2 notation=\<open>mixfix Case clause\<close>\<close>_ =>/ _)\<close> 10)
 
 translations
   "_Case_syntax x ms" == "CONST cases\<cdot>(ms\<cdot>x)"