--- a/src/HOL/Analysis/Bochner_Integration.thy Wed Oct 02 10:34:41 2024 +0200
+++ b/src/HOL/Analysis/Bochner_Integration.thy Wed Oct 02 10:35:44 2024 +0200
@@ -890,7 +890,8 @@
"integral\<^sup>L M f = (if \<exists>x. has_bochner_integral M f x then THE x. has_bochner_integral M f x else 0)"
syntax
- "_lebesgue_integral" :: "pttrn \<Rightarrow> real \<Rightarrow> 'a measure \<Rightarrow> real" (\<open>\<integral>((2 _./ _)/ \<partial>_)\<close> [60,61] 110)
+ "_lebesgue_integral" :: "pttrn \<Rightarrow> real \<Rightarrow> 'a measure \<Rightarrow> real"
+ (\<open>(\<open>indent=1 notation=\<open>binder integral\<close>\<close>\<integral>(2 _./ _)/ \<partial>_)\<close> [60,61] 110)
syntax_consts
"_lebesgue_integral" == lebesgue_integral
@@ -899,7 +900,8 @@
"\<integral> x. f \<partial>M" == "CONST lebesgue_integral M (\<lambda>x. f)"
syntax
- "_ascii_lebesgue_integral" :: "pttrn \<Rightarrow> 'a measure \<Rightarrow> real \<Rightarrow> real" (\<open>(3LINT (1_)/|(_)./ _)\<close> [0,110,60] 60)
+ "_ascii_lebesgue_integral" :: "pttrn \<Rightarrow> 'a measure \<Rightarrow> real \<Rightarrow> real"
+ (\<open>(\<open>indent=3 notation=\<open>mixfix LINT\<close>\<close>LINT (1_)/|(_)./ _)\<close> [0,110,60] 60)
syntax_consts
"_ascii_lebesgue_integral" == lebesgue_integral
--- a/src/HOL/Analysis/Bounded_Continuous_Function.thy Wed Oct 02 10:34:41 2024 +0200
+++ b/src/HOL/Analysis/Bounded_Continuous_Function.thy Wed Oct 02 10:35:44 2024 +0200
@@ -10,7 +10,7 @@
definition\<^marker>\<open>tag important\<close> "bcontfun = {f. continuous_on UNIV f \<and> bounded (range f)}"
-typedef (overloaded) ('a, 'b) bcontfun (\<open>(_ \<Rightarrow>\<^sub>C /_)\<close> [22, 21] 21) =
+typedef (overloaded) ('a, 'b) bcontfun (\<open>(\<open>notation=\<open>infix \<Rightarrow>\<^sub>C\<close>\<close>_ \<Rightarrow>\<^sub>C /_)\<close> [22, 21] 21) =
"bcontfun::('a::topological_space \<Rightarrow> 'b::metric_space) set"
morphisms apply_bcontfun Bcontfun
by (auto intro: continuous_intros simp: bounded_def bcontfun_def)
--- a/src/HOL/Analysis/Bounded_Linear_Function.thy Wed Oct 02 10:34:41 2024 +0200
+++ b/src/HOL/Analysis/Bounded_Linear_Function.thy Wed Oct 02 10:35:44 2024 +0200
@@ -116,7 +116,7 @@
subsection \<open>Type of bounded linear functions\<close>
-typedef\<^marker>\<open>tag important\<close> (overloaded) ('a, 'b) blinfun (\<open>(_ \<Rightarrow>\<^sub>L /_)\<close> [22, 21] 21) =
+typedef\<^marker>\<open>tag important\<close> (overloaded) ('a, 'b) blinfun (\<open>(\<open>notation=\<open>infix \<Rightarrow>\<^sub>L\<close>\<close>_ \<Rightarrow>\<^sub>L /_)\<close> [22, 21] 21) =
"{f::'a::real_normed_vector\<Rightarrow>'b::real_normed_vector. bounded_linear f}"
morphisms blinfun_apply Blinfun
by (blast intro: bounded_linear_intros)
--- a/src/HOL/Analysis/Finite_Product_Measure.thy Wed Oct 02 10:34:41 2024 +0200
+++ b/src/HOL/Analysis/Finite_Product_Measure.thy Wed Oct 02 10:35:44 2024 +0200
@@ -169,7 +169,8 @@
"Pi\<^sub>M I M \<equiv> PiM I M"
syntax
- "_PiM" :: "pttrn \<Rightarrow> 'i set \<Rightarrow> 'a measure \<Rightarrow> ('i => 'a) measure" (\<open>(3\<Pi>\<^sub>M _\<in>_./ _)\<close> 10)
+ "_PiM" :: "pttrn \<Rightarrow> 'i set \<Rightarrow> 'a measure \<Rightarrow> ('i => 'a) measure"
+ (\<open>(\<open>indent=3 notation=\<open>binder \<Pi>\<^sub>M\<close>\<close>\<Pi>\<^sub>M _\<in>_./ _)\<close> 10)
syntax_consts
"_PiM" == PiM
translations
--- a/src/HOL/Analysis/Infinite_Set_Sum.thy Wed Oct 02 10:34:41 2024 +0200
+++ b/src/HOL/Analysis/Infinite_Set_Sum.thy Wed Oct 02 10:35:44 2024 +0200
@@ -96,10 +96,10 @@
syntax (ASCII)
"_infsetsum" :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b \<Rightarrow> 'b::{banach, second_countable_topology}"
- (\<open>(3INFSETSUM _:_./ _)\<close> [0, 51, 10] 10)
+ (\<open>(\<open>indent=3 notation=\<open>binder INFSETSUM\<close>\<close>INFSETSUM _:_./ _)\<close> [0, 51, 10] 10)
syntax
"_infsetsum" :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b \<Rightarrow> 'b::{banach, second_countable_topology}"
- (\<open>(2\<Sum>\<^sub>a_\<in>_./ _)\<close> [0, 51, 10] 10)
+ (\<open>(\<open>indent=2 notation=\<open>binder \<Sum>\<^sub>a\<close>\<close>\<Sum>\<^sub>a_\<in>_./ _)\<close> [0, 51, 10] 10)
syntax_consts
"_infsetsum" \<rightleftharpoons> infsetsum
translations \<comment> \<open>Beware of argument permutation!\<close>
@@ -107,10 +107,10 @@
syntax (ASCII)
"_uinfsetsum" :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b \<Rightarrow> 'b::{banach, second_countable_topology}"
- (\<open>(3INFSETSUM _:_./ _)\<close> [0, 51, 10] 10)
+ (\<open>(\<open>indent=3 notation=\<open>binder INFSETSUM\<close>\<close>INFSETSUM _:_./ _)\<close> [0, 51, 10] 10)
syntax
"_uinfsetsum" :: "pttrn \<Rightarrow> 'b \<Rightarrow> 'b::{banach, second_countable_topology}"
- (\<open>(2\<Sum>\<^sub>a_./ _)\<close> [0, 10] 10)
+ (\<open>(\<open>indent=2 notation=\<open>binder \<Sum>\<^sub>a\<close>\<close>\<Sum>\<^sub>a_./ _)\<close> [0, 10] 10)
syntax_consts
"_uinfsetsum" \<rightleftharpoons> infsetsum
translations \<comment> \<open>Beware of argument permutation!\<close>
@@ -118,10 +118,10 @@
syntax (ASCII)
"_qinfsetsum" :: "pttrn \<Rightarrow> bool \<Rightarrow> 'a \<Rightarrow> 'a::{banach, second_countable_topology}"
- (\<open>(3INFSETSUM _ |/ _./ _)\<close> [0, 0, 10] 10)
+ (\<open>(\<open>indent=3 notation=\<open>binder INFSETSUM\<close>\<close>INFSETSUM _ |/ _./ _)\<close> [0, 0, 10] 10)
syntax
"_qinfsetsum" :: "pttrn \<Rightarrow> bool \<Rightarrow> 'a \<Rightarrow> 'a::{banach, second_countable_topology}"
- (\<open>(2\<Sum>\<^sub>a_ | (_)./ _)\<close> [0, 0, 10] 10)
+ (\<open>(\<open>indent=2 notation=\<open>binder \<Sum>\<^sub>a\<close>\<close>\<Sum>\<^sub>a_ | (_)./ _)\<close> [0, 0, 10] 10)
syntax_consts
"_qinfsetsum" \<rightleftharpoons> infsetsum
translations
--- a/src/HOL/Analysis/Infinite_Sum.thy Wed Oct 02 10:34:41 2024 +0200
+++ b/src/HOL/Analysis/Infinite_Sum.thy Wed Oct 02 10:35:44 2024 +0200
@@ -47,27 +47,29 @@
"f abs_summable_on A \<equiv> (\<lambda>x. norm (f x)) summable_on A"
syntax (ASCII)
- "_infsum" :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b \<Rightarrow> 'b::topological_comm_monoid_add" (\<open>(3INFSUM (_/:_)./ _)\<close> [0, 51, 10] 10)
+ "_infsum" :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b \<Rightarrow> 'b::topological_comm_monoid_add"
+ (\<open>(\<open>indent=3 notation=\<open>binder INFSUM\<close>\<close>INFSUM (_/:_)./ _)\<close> [0, 51, 10] 10)
syntax
- "_infsum" :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b \<Rightarrow> 'b::topological_comm_monoid_add" (\<open>(2\<Sum>\<^sub>\<infinity>(_/\<in>_)./ _)\<close> [0, 51, 10] 10)
+ "_infsum" :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b \<Rightarrow> 'b::topological_comm_monoid_add"
+ (\<open>(\<open>indent=2 notation=\<open>binder \<Sum>\<^sub>\<infinity>\<close>\<close>\<Sum>\<^sub>\<infinity>(_/\<in>_)./ _)\<close> [0, 51, 10] 10)
syntax_consts
"_infsum" \<rightleftharpoons> infsum
translations \<comment> \<open>Beware of argument permutation!\<close>
"\<Sum>\<^sub>\<infinity>i\<in>A. b" \<rightleftharpoons> "CONST infsum (\<lambda>i. b) A"
syntax (ASCII)
- "_univinfsum" :: "pttrn \<Rightarrow> 'a \<Rightarrow> 'a" (\<open>(3INFSUM _./ _)\<close> [0, 10] 10)
+ "_univinfsum" :: "pttrn \<Rightarrow> 'a \<Rightarrow> 'a" (\<open>(\<open>indent=3 notation=\<open>binder INFSUM\<close>\<close>INFSUM _./ _)\<close> [0, 10] 10)
syntax
- "_univinfsum" :: "pttrn \<Rightarrow> 'a \<Rightarrow> 'a" (\<open>(2\<Sum>\<^sub>\<infinity>_./ _)\<close> [0, 10] 10)
+ "_univinfsum" :: "pttrn \<Rightarrow> 'a \<Rightarrow> 'a" (\<open>(\<open>indent=2 notation=\<open>binder \<Sum>\<^sub>\<infinity>\<close>\<close>\<Sum>\<^sub>\<infinity>_./ _)\<close> [0, 10] 10)
syntax_consts
"_univinfsum" \<rightleftharpoons> infsum
translations
"\<Sum>\<^sub>\<infinity>x. t" \<rightleftharpoons> "CONST infsum (\<lambda>x. t) (CONST UNIV)"
syntax (ASCII)
- "_qinfsum" :: "pttrn \<Rightarrow> bool \<Rightarrow> 'a \<Rightarrow> 'a" (\<open>(3INFSUM _ |/ _./ _)\<close> [0, 0, 10] 10)
+ "_qinfsum" :: "pttrn \<Rightarrow> bool \<Rightarrow> 'a \<Rightarrow> 'a" (\<open>(\<open>indent=3 notation=\<open>binder INFSUM\<close>\<close>INFSUM _ |/ _./ _)\<close> [0, 0, 10] 10)
syntax
- "_qinfsum" :: "pttrn \<Rightarrow> bool \<Rightarrow> 'a \<Rightarrow> 'a" (\<open>(2\<Sum>\<^sub>\<infinity>_ | (_)./ _)\<close> [0, 0, 10] 10)
+ "_qinfsum" :: "pttrn \<Rightarrow> bool \<Rightarrow> 'a \<Rightarrow> 'a" (\<open>(\<open>indent=2 notation=\<open>binder \<Sum>\<^sub>\<infinity>\<close>\<close>\<Sum>\<^sub>\<infinity>_ | (_)./ _)\<close> [0, 0, 10] 10)
syntax_consts
"_qinfsum" \<rightleftharpoons> infsum
translations
--- a/src/HOL/Analysis/Inner_Product.thy Wed Oct 02 10:34:41 2024 +0200
+++ b/src/HOL/Analysis/Inner_Product.thy Wed Oct 02 10:35:44 2024 +0200
@@ -391,9 +391,8 @@
subsection \<open>Gradient derivative\<close>
definition\<^marker>\<open>tag important\<close>
- gderiv ::
- "['a::real_inner \<Rightarrow> real, 'a, 'a] \<Rightarrow> bool"
- (\<open>(GDERIV (_)/ (_)/ :> (_))\<close> [1000, 1000, 60] 60)
+ gderiv :: "['a::real_inner \<Rightarrow> real, 'a, 'a] \<Rightarrow> bool"
+ (\<open>(\<open>notation=\<open>mixfix GDERIV\<close>\<close>GDERIV (_)/ (_)/ :> (_))\<close> [1000, 1000, 60] 60)
where
"GDERIV f x :> D \<longleftrightarrow> FDERIV f x :> (\<lambda>h. inner h D)"
--- a/src/HOL/Analysis/Interval_Integral.thy Wed Oct 02 10:34:41 2024 +0200
+++ b/src/HOL/Analysis/Interval_Integral.thy Wed Oct 02 10:35:44 2024 +0200
@@ -146,7 +146,7 @@
syntax
"_ascii_interval_lebesgue_integral" :: "pttrn \<Rightarrow> real \<Rightarrow> real \<Rightarrow> real measure \<Rightarrow> real \<Rightarrow> real"
- (\<open>(5LINT _=_.._|_. _)\<close> [0,60,60,61,100] 60)
+ (\<open>(\<open>indent=5 notation=\<open>binder LINT\<close>\<close>LINT _=_.._|_. _)\<close> [0,60,60,61,100] 60)
syntax_consts
"_ascii_interval_lebesgue_integral" == interval_lebesgue_integral
@@ -160,7 +160,7 @@
syntax
"_ascii_interval_lebesgue_borel_integral" :: "pttrn \<Rightarrow> real \<Rightarrow> real \<Rightarrow> real \<Rightarrow> real"
- (\<open>(4LBINT _=_.._. _)\<close> [0,60,60,61] 60)
+ (\<open>(\<open>indent=4 notation=\<open>binder LBINT\<close>\<close>LBINT _=_.._. _)\<close> [0,60,60,61] 60)
syntax_consts
"_ascii_interval_lebesgue_borel_integral" == interval_lebesgue_integral
@@ -1049,7 +1049,7 @@
syntax "_complex_lebesgue_borel_integral" :: "pttrn \<Rightarrow> real \<Rightarrow> complex"
- (\<open>(2CLBINT _. _)\<close> [0,60] 60)
+ (\<open>(\<open>indent=2 notation=\<open>binder CLBINT\<close>\<close>CLBINT _. _)\<close> [0,60] 60)
syntax_consts
"_complex_lebesgue_borel_integral" == complex_lebesgue_integral
@@ -1057,7 +1057,7 @@
translations "CLBINT x. f" == "CONST complex_lebesgue_integral CONST lborel (\<lambda>x. f)"
syntax "_complex_set_lebesgue_borel_integral" :: "pttrn \<Rightarrow> real set \<Rightarrow> real \<Rightarrow> complex"
- (\<open>(3CLBINT _:_. _)\<close> [0,60,61] 60)
+ (\<open>(\<open>indent=3 notation=\<open>binder CLBINT\<close>\<close>CLBINT _:_. _)\<close> [0,60,61] 60)
syntax_consts
"_complex_set_lebesgue_borel_integral" == complex_set_lebesgue_integral
@@ -1075,7 +1075,7 @@
syntax
"_ascii_complex_interval_lebesgue_borel_integral" :: "pttrn \<Rightarrow> ereal \<Rightarrow> ereal \<Rightarrow> real \<Rightarrow> complex"
- (\<open>(4CLBINT _=_.._. _)\<close> [0,60,60,61] 60)
+ (\<open>(\<open>indent=4 notation=\<open>binder CLBINT\<close>\<close>CLBINT _=_.._. _)\<close> [0,60,60,61] 60)
syntax_consts
"_ascii_complex_interval_lebesgue_borel_integral" == complex_interval_lebesgue_integral
--- a/src/HOL/Analysis/Nonnegative_Lebesgue_Integration.thy Wed Oct 02 10:34:41 2024 +0200
+++ b/src/HOL/Analysis/Nonnegative_Lebesgue_Integration.thy Wed Oct 02 10:35:44 2024 +0200
@@ -820,7 +820,7 @@
"integral\<^sup>N M f = (SUP g \<in> {g. simple_function M g \<and> g \<le> f}. integral\<^sup>S M g)"
syntax
- "_nn_integral" :: "pttrn \<Rightarrow> ennreal \<Rightarrow> 'a measure \<Rightarrow> ennreal" (\<open>\<integral>\<^sup>+((2 _./ _)/ \<partial>_)\<close> [60,61] 110)
+ "_nn_integral" :: "pttrn \<Rightarrow> ennreal \<Rightarrow> 'a measure \<Rightarrow> ennreal" (\<open>(\<open>indent=2 notation=\<open>binder integral\<close>\<close>\<integral>\<^sup>+(2 _./ _)/ \<partial>_)\<close> [60,61] 110)
syntax_consts
"_nn_integral" == nn_integral
--- a/src/HOL/Analysis/Set_Integral.thy Wed Oct 02 10:34:41 2024 +0200
+++ b/src/HOL/Analysis/Set_Integral.thy Wed Oct 02 10:35:44 2024 +0200
@@ -24,7 +24,7 @@
syntax
"_ascii_set_lebesgue_integral" :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'a measure \<Rightarrow> real \<Rightarrow> real"
- (\<open>(4LINT (_):(_)/|(_)./ _)\<close> [0,0,0,10] 10)
+ (\<open>(\<open>indent=4 notation=\<open>binder LINT\<close>\<close>LINT (_):(_)/|(_)./ _)\<close> [0,0,0,10] 10)
syntax_consts
"_ascii_set_lebesgue_integral" == set_lebesgue_integral
@@ -43,11 +43,11 @@
syntax
"_lebesgue_borel_integral" :: "pttrn \<Rightarrow> real \<Rightarrow> real"
- (\<open>(2LBINT _./ _)\<close> [0,10] 10)
+ (\<open>(\<open>indent=2 notation=\<open>binder LBINT\<close>\<close>LBINT _./ _)\<close> [0,10] 10)
syntax
"_set_lebesgue_borel_integral" :: "pttrn \<Rightarrow> real set \<Rightarrow> real \<Rightarrow> real"
- (\<open>(3LBINT _:_./ _)\<close> [0,0,10] 10)
+ (\<open>(\<open>indent=3 notation=\<open>binder LBINT\<close>\<close>LBINT _:_./ _)\<close> [0,0,10] 10)
section \<open>Basic properties\<close>
@@ -587,7 +587,7 @@
syntax
"_ascii_complex_lebesgue_integral" :: "pttrn \<Rightarrow> 'a measure \<Rightarrow> real \<Rightarrow> real"
- (\<open>(3CLINT _|_. _)\<close> [0,0,10] 10)
+ (\<open>(\<open>indent=3 notation=\<open>binder CLINT\<close>\<close>CLINT _|_. _)\<close> [0,0,10] 10)
syntax_consts
"_ascii_complex_lebesgue_integral" == complex_lebesgue_integral
@@ -624,7 +624,7 @@
syntax
"_ascii_complex_set_lebesgue_integral" :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'a measure \<Rightarrow> real \<Rightarrow> real"
- (\<open>(4CLINT _:_|_. _)\<close> [0,0,0,10] 10)
+ (\<open>(\<open>indent=4 notation=\<open>binder CLINT\<close>\<close>CLINT _:_|_. _)\<close> [0,0,0,10] 10)
syntax_consts
"_ascii_complex_set_lebesgue_integral" == complex_set_lebesgue_integral
@@ -647,10 +647,10 @@
syntax
"_set_nn_integral" :: "pttrn => 'a set => 'a measure => ereal => ereal"
-(\<open>(\<integral>\<^sup>+((_)\<in>(_)./ _)/\<partial>_)\<close> [0,0,0,110] 10)
+(\<open>(\<open>notation=\<open>binder integral\<close>\<close>\<integral>\<^sup>+((_)\<in>(_)./ _)/\<partial>_)\<close> [0,0,0,110] 10)
"_set_lebesgue_integral" :: "pttrn => 'a set => 'a measure => ereal => ereal"
-(\<open>(\<integral>((_)\<in>(_)./ _)/\<partial>_)\<close> [0,0,0,110] 10)
+(\<open>(\<open>notation=\<open>binder integral\<close>\<close>\<integral>((_)\<in>(_)./ _)/\<partial>_)\<close> [0,0,0,110] 10)
syntax_consts
"_set_nn_integral" == set_nn_integral and
--- a/src/HOL/Analysis/Sparse_In.thy Wed Oct 02 10:34:41 2024 +0200
+++ b/src/HOL/Analysis/Sparse_In.thy Wed Oct 02 10:35:44 2024 +0200
@@ -165,14 +165,14 @@
"cosparse A = Abs_filter (\<lambda>P. {x. \<not>P x} sparse_in A)"
syntax
- "_eventually_cosparse" :: "pttrn => 'a set => bool => bool" (\<open>(3\<forall>\<^sub>\<approx>_\<in>_./ _)\<close> [0, 0, 10] 10)
+ "_eventually_cosparse" :: "pttrn => 'a set => bool => bool" (\<open>(\<open>indent=3 notation=\<open>binder \<forall>\<approx>\<close>\<close>\<forall>\<^sub>\<approx>_\<in>_./ _)\<close> [0, 0, 10] 10)
syntax_consts
"_eventually_cosparse" == eventually
translations
"\<forall>\<^sub>\<approx>x\<in>A. P" == "CONST eventually (\<lambda>x. P) (CONST cosparse A)"
syntax
- "_qeventually_cosparse" :: "pttrn \<Rightarrow> bool \<Rightarrow> 'a \<Rightarrow> 'a" (\<open>(3\<forall>\<^sub>\<approx>_ | (_)./ _)\<close> [0, 0, 10] 10)
+ "_qeventually_cosparse" :: "pttrn \<Rightarrow> bool \<Rightarrow> 'a \<Rightarrow> 'a" (\<open>(\<open>indent=3 notation=\<open>binder \<forall>\<approx>\<close>\<close>\<forall>\<^sub>\<approx>_ | (_)./ _)\<close> [0, 0, 10] 10)
syntax_consts
"_qeventually_cosparse" == eventually
translations