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