--- a/src/HOL/BNF_Cardinal_Arithmetic.thy Mon Sep 23 15:01:10 2024 +0200
+++ b/src/HOL/BNF_Cardinal_Arithmetic.thy Mon Sep 23 21:09:23 2024 +0200
@@ -273,7 +273,7 @@
(* Similar setup to the one for SIGMA from theory Big_Operators: *)
syntax "_Csum" ::
"pttrn => ('a * 'a) set => 'b * 'b set => (('a * 'b) * ('a * 'b)) set"
- (\<open>(3CSUM _:_. _)\<close> [0, 51, 10] 10)
+ (\<open>(\<open>indent=3 notation=\<open>binder CSUM\<close>\<close>CSUM _:_. _)\<close> [0, 51, 10] 10)
syntax_consts
"_Csum" == Csum
--- a/src/HOL/Complete_Lattices.thy Mon Sep 23 15:01:10 2024 +0200
+++ b/src/HOL/Complete_Lattices.thy Mon Sep 23 21:09:23 2024 +0200
@@ -21,16 +21,16 @@
fixes Sup :: "'a set \<Rightarrow> 'a" (\<open>\<Squnion> _\<close> [900] 900)
syntax
- "_INF1" :: "pttrns \<Rightarrow> 'b \<Rightarrow> 'b" (\<open>(3INF _./ _)\<close> [0, 10] 10)
- "_INF" :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b \<Rightarrow> 'b" (\<open>(3INF _\<in>_./ _)\<close> [0, 0, 10] 10)
- "_SUP1" :: "pttrns \<Rightarrow> 'b \<Rightarrow> 'b" (\<open>(3SUP _./ _)\<close> [0, 10] 10)
- "_SUP" :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b \<Rightarrow> 'b" (\<open>(3SUP _\<in>_./ _)\<close> [0, 0, 10] 10)
+ "_INF1" :: "pttrns \<Rightarrow> 'b \<Rightarrow> 'b" (\<open>(\<open>indent=3 notation=\<open>binder INF\<close>\<close>INF _./ _)\<close> [0, 10] 10)
+ "_INF" :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b \<Rightarrow> 'b" (\<open>(\<open>indent=3 notation=\<open>binder INF\<close>\<close>INF _\<in>_./ _)\<close> [0, 0, 10] 10)
+ "_SUP1" :: "pttrns \<Rightarrow> 'b \<Rightarrow> 'b" (\<open>(\<open>indent=3 notation=\<open>binder SUP\<close>\<close>SUP _./ _)\<close> [0, 10] 10)
+ "_SUP" :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b \<Rightarrow> 'b" (\<open>(\<open>indent=3 notation=\<open>binder SUP\<close>\<close>SUP _\<in>_./ _)\<close> [0, 0, 10] 10)
syntax
- "_INF1" :: "pttrns \<Rightarrow> 'b \<Rightarrow> 'b" (\<open>(3\<Sqinter>_./ _)\<close> [0, 10] 10)
- "_INF" :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b \<Rightarrow> 'b" (\<open>(3\<Sqinter>_\<in>_./ _)\<close> [0, 0, 10] 10)
- "_SUP1" :: "pttrns \<Rightarrow> 'b \<Rightarrow> 'b" (\<open>(3\<Squnion>_./ _)\<close> [0, 10] 10)
- "_SUP" :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b \<Rightarrow> 'b" (\<open>(3\<Squnion>_\<in>_./ _)\<close> [0, 0, 10] 10)
+ "_INF1" :: "pttrns \<Rightarrow> 'b \<Rightarrow> 'b" (\<open>(\<open>indent=3 notation=\<open>binder \<Sqinter>\<close>\<close>\<Sqinter>_./ _)\<close> [0, 10] 10)
+ "_INF" :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b \<Rightarrow> 'b" (\<open>(\<open>indent=3 notation=\<open>binder \<Sqinter>\<close>\<close>\<Sqinter>_\<in>_./ _)\<close> [0, 0, 10] 10)
+ "_SUP1" :: "pttrns \<Rightarrow> 'b \<Rightarrow> 'b" (\<open>(\<open>indent=3 notation=\<open>binder \<Squnion>\<close>\<close>\<Squnion>_./ _)\<close> [0, 10] 10)
+ "_SUP" :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b \<Rightarrow> 'b" (\<open>(\<open>indent=3 notation=\<open>binder \<Squnion>\<close>\<close>\<Squnion>_\<in>_./ _)\<close> [0, 0, 10] 10)
syntax_consts
"_INF1" "_INF" \<rightleftharpoons> Inf and
@@ -843,12 +843,12 @@
subsubsection \<open>Intersections of families\<close>
syntax (ASCII)
- "_INTER1" :: "pttrns \<Rightarrow> 'b set \<Rightarrow> 'b set" (\<open>(3INT _./ _)\<close> [0, 10] 10)
- "_INTER" :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b set \<Rightarrow> 'b set" (\<open>(3INT _:_./ _)\<close> [0, 0, 10] 10)
+ "_INTER1" :: "pttrns \<Rightarrow> 'b set \<Rightarrow> 'b set" (\<open>(\<open>indent=3 notation=\<open>binder INT\<close>\<close>INT _./ _)\<close> [0, 10] 10)
+ "_INTER" :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b set \<Rightarrow> 'b set" (\<open>(\<open>indent=3 notation=\<open>binder INT\<close>\<close>INT _:_./ _)\<close> [0, 0, 10] 10)
syntax
- "_INTER1" :: "pttrns \<Rightarrow> 'b set \<Rightarrow> 'b set" (\<open>(3\<Inter>_./ _)\<close> [0, 10] 10)
- "_INTER" :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b set \<Rightarrow> 'b set" (\<open>(3\<Inter>_\<in>_./ _)\<close> [0, 0, 10] 10)
+ "_INTER1" :: "pttrns \<Rightarrow> 'b set \<Rightarrow> 'b set" (\<open>(\<open>indent=3 notation=\<open>binder \<Inter>\<close>\<close>\<Inter>_./ _)\<close> [0, 10] 10)
+ "_INTER" :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b set \<Rightarrow> 'b set" (\<open>(\<open>indent=3 notation=\<open>binder \<Inter>\<close>\<close>\<Inter>_\<in>_./ _)\<close> [0, 0, 10] 10)
syntax (latex output)
"_INTER1" :: "pttrns \<Rightarrow> 'b set \<Rightarrow> 'b set" (\<open>(3\<Inter>(\<open>unbreakable\<close>\<^bsub>_\<^esub>)/ _)\<close> [0, 10] 10)
@@ -1009,12 +1009,12 @@
subsubsection \<open>Unions of families\<close>
syntax (ASCII)
- "_UNION1" :: "pttrns => 'b set => 'b set" (\<open>(3UN _./ _)\<close> [0, 10] 10)
- "_UNION" :: "pttrn => 'a set => 'b set => 'b set" (\<open>(3UN _:_./ _)\<close> [0, 0, 10] 10)
+ "_UNION1" :: "pttrns => 'b set => 'b set" (\<open>(\<open>indent=3 notation=\<open>binder UN\<close>\<close>UN _./ _)\<close> [0, 10] 10)
+ "_UNION" :: "pttrn => 'a set => 'b set => 'b set" (\<open>(\<open>indent=3 notation=\<open>binder UN\<close>\<close>UN _:_./ _)\<close> [0, 0, 10] 10)
syntax
- "_UNION1" :: "pttrns => 'b set => 'b set" (\<open>(3\<Union>_./ _)\<close> [0, 10] 10)
- "_UNION" :: "pttrn => 'a set => 'b set => 'b set" (\<open>(3\<Union>_\<in>_./ _)\<close> [0, 0, 10] 10)
+ "_UNION1" :: "pttrns => 'b set => 'b set" (\<open>(\<open>indent=3 notation=\<open>binder \<Union>\<close>\<close>\<Union>_./ _)\<close> [0, 10] 10)
+ "_UNION" :: "pttrn => 'a set => 'b set => 'b set" (\<open>(\<open>indent=3 notation=\<open>binder \<Union>\<close>\<close>\<Union>_\<in>_./ _)\<close> [0, 0, 10] 10)
syntax (latex output)
"_UNION1" :: "pttrns => 'b set => 'b set" (\<open>(3\<Union>(\<open>unbreakable\<close>\<^bsub>_\<^esub>)/ _)\<close> [0, 10] 10)
--- a/src/HOL/Deriv.thy Mon Sep 23 15:01:10 2024 +0200
+++ b/src/HOL/Deriv.thy Mon Sep 23 21:09:23 2024 +0200
@@ -70,7 +70,7 @@
\<close>
abbreviation (input)
FDERIV :: "('a::real_normed_vector \<Rightarrow> 'b::real_normed_vector) \<Rightarrow> 'a \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> bool"
- (\<open>(FDERIV (_)/ (_)/ :> (_))\<close> [1000, 1000, 60] 60)
+ (\<open>(\<open>notation=\<open>mixfix FDERIV\<close>\<close>FDERIV (_)/ (_)/ :> (_))\<close> [1000, 1000, 60] 60)
where "FDERIV f x :> f' \<equiv> (f has_derivative f') (at x)"
lemma has_derivative_bounded_linear: "(f has_derivative f') F \<Longrightarrow> bounded_linear f'"
@@ -782,7 +782,7 @@
abbreviation (input)
DERIV :: "('a::real_normed_field \<Rightarrow> 'a) \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> bool"
- (\<open>(DERIV (_)/ (_)/ :> (_))\<close> [1000, 1000, 60] 60)
+ (\<open>(\<open>notation=\<open>mixfix DERIV\<close>\<close>DERIV (_)/ (_)/ :> (_))\<close> [1000, 1000, 60] 60)
where "DERIV f x :> D \<equiv> (f has_field_derivative D) (at x)"
abbreviation has_real_derivative :: "(real \<Rightarrow> real) \<Rightarrow> real \<Rightarrow> real filter \<Rightarrow> bool"
--- a/src/HOL/Filter.thy Mon Sep 23 15:01:10 2024 +0200
+++ b/src/HOL/Filter.thy Mon Sep 23 21:09:23 2024 +0200
@@ -40,7 +40,7 @@
where "eventually P F \<longleftrightarrow> Rep_filter F P"
syntax
- "_eventually" :: "pttrn => 'a filter => bool => bool" (\<open>(3\<forall>\<^sub>F _ in _./ _)\<close> [0, 0, 10] 10)
+ "_eventually" :: "pttrn => 'a filter => bool => bool" (\<open>(\<open>indent=3 notation=\<open>binder \<forall>\<^sub>F\<close>\<close>\<forall>\<^sub>F _ in _./ _)\<close> [0, 0, 10] 10)
syntax_consts
"_eventually" == eventually
translations
@@ -160,7 +160,7 @@
where "frequently P F \<longleftrightarrow> \<not> eventually (\<lambda>x. \<not> P x) F"
syntax
- "_frequently" :: "pttrn \<Rightarrow> 'a filter \<Rightarrow> bool \<Rightarrow> bool" (\<open>(3\<exists>\<^sub>F _ in _./ _)\<close> [0, 0, 10] 10)
+ "_frequently" :: "pttrn \<Rightarrow> 'a filter \<Rightarrow> bool \<Rightarrow> bool" (\<open>(\<open>indent=3 notation=\<open>binder \<exists>\<^sub>F\<close>\<close>\<exists>\<^sub>F _ in _./ _)\<close> [0, 0, 10] 10)
syntax_consts
"_frequently" == frequently
translations
@@ -1307,7 +1307,7 @@
"filterlim f F2 F1 \<longleftrightarrow> filtermap f F1 \<le> F2"
syntax
- "_LIM" :: "pttrns \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'a \<Rightarrow> bool" (\<open>(3LIM (_)/ (_)./ (_) :> (_))\<close> [1000, 10, 0, 10] 10)
+ "_LIM" :: "pttrns \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'a \<Rightarrow> bool" (\<open>(\<open>indent=3 notation=\<open>binder LIM\<close>\<close>LIM (_)/ (_)./ (_) :> (_))\<close> [1000, 10, 0, 10] 10)
syntax_consts
"_LIM" == filterlim
--- a/src/HOL/Fun.thy Mon Sep 23 15:01:10 2024 +0200
+++ b/src/HOL/Fun.thy Mon Sep 23 21:09:23 2024 +0200
@@ -841,10 +841,10 @@
nonterminal updbinds and updbind
syntax
- "_updbind" :: "'a \<Rightarrow> 'a \<Rightarrow> updbind" (\<open>(2_ :=/ _)\<close>)
+ "_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>_/'((_)')\<close> [1000, 0] 900)
+ "_Update" :: "'a \<Rightarrow> updbinds \<Rightarrow> 'a" (\<open>_/'((\<open>indent=2 notation=\<open>mixfix updates\<close>\<close>_)')\<close> [1000, 0] 900)
syntax_consts
"_updbind" "_updbinds" "_Update" \<rightleftharpoons> fun_upd
--- a/src/HOL/GCD.thy Mon Sep 23 15:01:10 2024 +0200
+++ b/src/HOL/GCD.thy Mon Sep 23 21:09:23 2024 +0200
@@ -148,10 +148,10 @@
and Lcm :: "'a set \<Rightarrow> 'a"
syntax
- "_GCD1" :: "pttrns \<Rightarrow> 'b \<Rightarrow> 'b" (\<open>(3GCD _./ _)\<close> [0, 10] 10)
- "_GCD" :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b \<Rightarrow> 'b" (\<open>(3GCD _\<in>_./ _)\<close> [0, 0, 10] 10)
- "_LCM1" :: "pttrns \<Rightarrow> 'b \<Rightarrow> 'b" (\<open>(3LCM _./ _)\<close> [0, 10] 10)
- "_LCM" :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b \<Rightarrow> 'b" (\<open>(3LCM _\<in>_./ _)\<close> [0, 0, 10] 10)
+ "_GCD1" :: "pttrns \<Rightarrow> 'b \<Rightarrow> 'b" (\<open>(\<open>indent=3 notation=\<open>binder GCD\<close>\<close>GCD _./ _)\<close> [0, 10] 10)
+ "_GCD" :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b \<Rightarrow> 'b" (\<open>(\<open>indent=3 notation=\<open>binder GCD\<close>\<close>GCD _\<in>_./ _)\<close> [0, 0, 10] 10)
+ "_LCM1" :: "pttrns \<Rightarrow> 'b \<Rightarrow> 'b" (\<open>(\<open>indent=3 notation=\<open>binder LCM\<close>\<close>LCM _./ _)\<close> [0, 10] 10)
+ "_LCM" :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b \<Rightarrow> 'b" (\<open>(\<open>indent=3 notation=\<open>binder LCM\<close>\<close>LCM _\<in>_./ _)\<close> [0, 0, 10] 10)
syntax_consts
"_GCD1" "_GCD" \<rightleftharpoons> Gcd and
@@ -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>(1CHAR/(1'(_')))\<close>)
+syntax "_type_char" :: "type => nat" (\<open>(\<open>indent=1 notation=\<open>prefix 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>
--- a/src/HOL/Groups_Big.thy Mon Sep 23 15:01:10 2024 +0200
+++ b/src/HOL/Groups_Big.thy Mon Sep 23 21:09:23 2024 +0200
@@ -651,9 +651,9 @@
text \<open>Now: lots of fancy syntax. First, \<^term>\<open>sum (\<lambda>x. e) A\<close> is written \<open>\<Sum>x\<in>A. e\<close>.\<close>
syntax (ASCII)
- "_sum" :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b \<Rightarrow> 'b::comm_monoid_add" (\<open>(3SUM (_/:_)./ _)\<close> [0, 51, 10] 10)
+ "_sum" :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b \<Rightarrow> 'b::comm_monoid_add" (\<open>(\<open>indent=3 notation=\<open>binder SUM\<close>\<close>SUM (_/:_)./ _)\<close> [0, 51, 10] 10)
syntax
- "_sum" :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b \<Rightarrow> 'b::comm_monoid_add" (\<open>(2\<Sum>(_/\<in>_)./ _)\<close> [0, 51, 10] 10)
+ "_sum" :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b \<Rightarrow> 'b::comm_monoid_add" (\<open>(\<open>indent=2 notation=\<open>binder \<Sum>\<close>\<close>\<Sum>(_/\<in>_)./ _)\<close> [0, 51, 10] 10)
syntax_consts
"_sum" \<rightleftharpoons> sum
@@ -665,9 +665,9 @@
text \<open>Instead of \<^term>\<open>\<Sum>x\<in>{x. P}. e\<close> we introduce the shorter \<open>\<Sum>x|P. e\<close>.\<close>
syntax (ASCII)
- "_qsum" :: "pttrn \<Rightarrow> bool \<Rightarrow> 'a \<Rightarrow> 'a" (\<open>(3SUM _ |/ _./ _)\<close> [0, 0, 10] 10)
+ "_qsum" :: "pttrn \<Rightarrow> bool \<Rightarrow> 'a \<Rightarrow> 'a" (\<open>(\<open>indent=3 notation=\<open>binder SUM Collect\<close>\<close>SUM _ |/ _./ _)\<close> [0, 0, 10] 10)
syntax
- "_qsum" :: "pttrn \<Rightarrow> bool \<Rightarrow> 'a \<Rightarrow> 'a" (\<open>(2\<Sum>_ | (_)./ _)\<close> [0, 0, 10] 10)
+ "_qsum" :: "pttrn \<Rightarrow> bool \<Rightarrow> 'a \<Rightarrow> 'a" (\<open>(\<open>indent=2 notation=\<open>binder \<Sum> Collect\<close>\<close>\<Sum>_ | (_)./ _)\<close> [0, 0, 10] 10)
syntax_consts
"_qsum" == sum
@@ -1421,9 +1421,9 @@
end
syntax (ASCII)
- "_prod" :: "pttrn => 'a set => 'b => 'b::comm_monoid_mult" (\<open>(4PROD (_/:_)./ _)\<close> [0, 51, 10] 10)
+ "_prod" :: "pttrn => 'a set => 'b => 'b::comm_monoid_mult" (\<open>(\<open>indent=4 notation=\<open>binder PROD\<close>\<close>PROD (_/:_)./ _)\<close> [0, 51, 10] 10)
syntax
- "_prod" :: "pttrn => 'a set => 'b => 'b::comm_monoid_mult" (\<open>(2\<Prod>(_/\<in>_)./ _)\<close> [0, 51, 10] 10)
+ "_prod" :: "pttrn => 'a set => 'b => 'b::comm_monoid_mult" (\<open>(\<open>indent=2 notation=\<open>binder \<Prod>\<close>\<close>\<Prod>(_/\<in>_)./ _)\<close> [0, 51, 10] 10)
syntax_consts
"_prod" == prod
@@ -1435,9 +1435,9 @@
text \<open>Instead of \<^term>\<open>\<Prod>x\<in>{x. P}. e\<close> we introduce the shorter \<open>\<Prod>x|P. e\<close>.\<close>
syntax (ASCII)
- "_qprod" :: "pttrn \<Rightarrow> bool \<Rightarrow> 'a \<Rightarrow> 'a" (\<open>(4PROD _ |/ _./ _)\<close> [0, 0, 10] 10)
+ "_qprod" :: "pttrn \<Rightarrow> bool \<Rightarrow> 'a \<Rightarrow> 'a" (\<open>(\<open>indent=4 notation=\<open>binder PROD Collect\<close>\<close>PROD _ |/ _./ _)\<close> [0, 0, 10] 10)
syntax
- "_qprod" :: "pttrn \<Rightarrow> bool \<Rightarrow> 'a \<Rightarrow> 'a" (\<open>(2\<Prod>_ | (_)./ _)\<close> [0, 0, 10] 10)
+ "_qprod" :: "pttrn \<Rightarrow> bool \<Rightarrow> 'a \<Rightarrow> 'a" (\<open>(\<open>indent=2 notation=\<open>binder \<Prod> Collect\<close>\<close>\<Prod>_ | (_)./ _)\<close> [0, 0, 10] 10)
syntax_consts
"_qprod" == prod
--- a/src/HOL/Groups_List.thy Mon Sep 23 15:01:10 2024 +0200
+++ b/src/HOL/Groups_List.thy Mon Sep 23 21:09:23 2024 +0200
@@ -98,9 +98,9 @@
text \<open>Some syntactic sugar for summing a function over a list:\<close>
syntax (ASCII)
- "_sum_list" :: "pttrn => 'a list => 'b => 'b" (\<open>(3SUM _<-_. _)\<close> [0, 51, 10] 10)
+ "_sum_list" :: "pttrn => 'a list => 'b => 'b" (\<open>(\<open>indent=3 notation=\<open>binder SUM\<close>\<close>SUM _<-_. _)\<close> [0, 51, 10] 10)
syntax
- "_sum_list" :: "pttrn => 'a list => 'b => 'b" (\<open>(3\<Sum>_\<leftarrow>_. _)\<close> [0, 51, 10] 10)
+ "_sum_list" :: "pttrn => 'a list => 'b => 'b" (\<open>(\<open>indent=3 notation=\<open>binder \<Sum>\<close>\<close>\<Sum>_\<leftarrow>_. _)\<close> [0, 51, 10] 10)
syntax_consts
"_sum_list" == sum_list
translations \<comment> \<open>Beware of argument permutation!\<close>
@@ -597,9 +597,9 @@
text \<open>Some syntactic sugar:\<close>
syntax (ASCII)
- "_prod_list" :: "pttrn => 'a list => 'b => 'b" (\<open>(3PROD _<-_. _)\<close> [0, 51, 10] 10)
+ "_prod_list" :: "pttrn => 'a list => 'b => 'b" (\<open>(\<open>indent=3 notation=\<open>binder PROD\<close>\<close>PROD _<-_. _)\<close> [0, 51, 10] 10)
syntax
- "_prod_list" :: "pttrn => 'a list => 'b => 'b" (\<open>(3\<Prod>_\<leftarrow>_. _)\<close> [0, 51, 10] 10)
+ "_prod_list" :: "pttrn => 'a list => 'b => 'b" (\<open>(\<open>indent=3 notation=\<open>binder \<Prod>\<close>\<close>\<Prod>_\<leftarrow>_. _)\<close> [0, 51, 10] 10)
syntax_consts
"_prod_list" \<rightleftharpoons> prod_list
translations \<comment> \<open>Beware of argument permutation!\<close>
--- a/src/HOL/HOL.thy Mon Sep 23 15:01:10 2024 +0200
+++ b/src/HOL/HOL.thy Mon Sep 23 21:09:23 2024 +0200
@@ -81,7 +81,7 @@
typedecl bool
-judgment Trueprop :: "bool \<Rightarrow> prop" (\<open>(_)\<close> 5)
+judgment Trueprop :: "bool \<Rightarrow> prop" (\<open>(\<open>notation=judgment\<close>_)\<close> 5)
axiomatization implies :: "[bool, bool] \<Rightarrow> bool" (infixr \<open>\<longrightarrow>\<close> 25)
and eq :: "['a, 'a] \<Rightarrow> bool"
@@ -127,8 +127,8 @@
subsubsection \<open>Additional concrete syntax\<close>
-syntax (ASCII) "_Uniq" :: "pttrn \<Rightarrow> bool \<Rightarrow> bool" (\<open>(4?< _./ _)\<close> [0, 10] 10)
-syntax "_Uniq" :: "pttrn \<Rightarrow> bool \<Rightarrow> bool" (\<open>(2\<exists>\<^sub>\<le>\<^sub>1 _./ _)\<close> [0, 10] 10)
+syntax (ASCII) "_Uniq" :: "pttrn \<Rightarrow> bool \<Rightarrow> bool" (\<open>(\<open>indent=4 notation=\<open>binder ?<\<close>\<close>?< _./ _)\<close> [0, 10] 10)
+syntax "_Uniq" :: "pttrn \<Rightarrow> bool \<Rightarrow> bool" (\<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
@@ -140,10 +140,10 @@
syntax (ASCII)
- "_Ex1" :: "pttrn \<Rightarrow> bool \<Rightarrow> bool" (\<open>(3EX! _./ _)\<close> [0, 10] 10)
+ "_Ex1" :: "pttrn \<Rightarrow> bool \<Rightarrow> bool" (\<open>(\<open>indent=3 notation=\<open>binder EX!\<close>\<close>EX! _./ _)\<close> [0, 10] 10)
syntax (input)
- "_Ex1" :: "pttrn \<Rightarrow> bool \<Rightarrow> bool" (\<open>(3?! _./ _)\<close> [0, 10] 10)
-syntax "_Ex1" :: "pttrn \<Rightarrow> bool \<Rightarrow> bool" (\<open>(3\<exists>!_./ _)\<close> [0, 10] 10)
+ "_Ex1" :: "pttrn \<Rightarrow> bool \<Rightarrow> bool" (\<open>(\<open>indent=3 notation=\<open>binder ?!\<close>\<close>?! _./ _)\<close> [0, 10] 10)
+syntax "_Ex1" :: "pttrn \<Rightarrow> bool \<Rightarrow> bool" (\<open>(\<open>indent=3 notation=\<open>binder \<exists>!\<close>\<close>\<exists>!_./ _)\<close> [0, 10] 10)
syntax_consts "_Ex1" \<rightleftharpoons> Ex1
@@ -155,8 +155,8 @@
syntax
- "_Not_Ex" :: "idts \<Rightarrow> bool \<Rightarrow> bool" (\<open>(3\<nexists>_./ _)\<close> [0, 10] 10)
- "_Not_Ex1" :: "pttrn \<Rightarrow> bool \<Rightarrow> bool" (\<open>(3\<nexists>!_./ _)\<close> [0, 10] 10)
+ "_Not_Ex" :: "idts \<Rightarrow> bool \<Rightarrow> bool" (\<open>(\<open>indent=3 notation=\<open>binder \<nexists>\<close>\<close>\<nexists>_./ _)\<close> [0, 10] 10)
+ "_Not_Ex1" :: "pttrn \<Rightarrow> bool \<Rightarrow> bool" (\<open>(\<open>indent=3 notation=\<open>binder \<nexists>!\<close>\<close>\<nexists>!_./ _)\<close> [0, 10] 10)
syntax_consts
"_Not_Ex" \<rightleftharpoons> Ex and
"_Not_Ex1" \<rightleftharpoons> Ex1
@@ -179,7 +179,7 @@
iff :: "[bool, bool] \<Rightarrow> bool" (infixr \<open>\<longleftrightarrow>\<close> 25)
where "A \<longleftrightarrow> B \<equiv> A = B"
-syntax "_The" :: "[pttrn, bool] \<Rightarrow> 'a" (\<open>(3THE _./ _)\<close> [0, 10] 10)
+syntax "_The" :: "[pttrn, bool] \<Rightarrow> 'a" (\<open>(\<open>indent=3 notation=\<open>binder THE\<close>\<close>THE _./ _)\<close> [0, 10] 10)
syntax_consts "_The" \<rightleftharpoons> The
translations "THE x. P" \<rightleftharpoons> "CONST The (\<lambda>x. P)"
print_translation \<open>
@@ -190,12 +190,12 @@
nonterminal case_syn and cases_syn
syntax
- "_case_syntax" :: "['a, cases_syn] \<Rightarrow> 'b" (\<open>(case _ of/ _)\<close> 10)
- "_case1" :: "['a, 'b] \<Rightarrow> case_syn" (\<open>(2_ \<Rightarrow>/ _)\<close> 10)
+ "_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 pattern\<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>(2_ =>/ _)\<close> 10)
+ "_case1" :: "['a, 'b] \<Rightarrow> case_syn" (\<open>(\<open>indent=2 notation=\<open>mixfix case pattern\<close>\<close>_ =>/ _)\<close> 10)
notation (ASCII)
All (binder \<open>ALL \<close> 10) and
@@ -224,7 +224,7 @@
True_or_False: "(P = True) \<or> (P = False)"
-definition If :: "bool \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'a" (\<open>(if (_)/ then (_)/ else (_))\<close> [0, 0, 10] 10)
+definition If :: "bool \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'a" (\<open>(\<open>notation=\<open>mixfix if expression\<close>\<close>if (_)/ then (_)/ else (_))\<close> [0, 0, 10] 10)
where "If P x y \<equiv> (THE z::'a. (P = True \<longrightarrow> z = x) \<and> (P = False \<longrightarrow> z = y))"
definition Let :: "'a \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> 'b"
@@ -232,10 +232,10 @@
nonterminal letbinds and letbind
syntax
- "_bind" :: "[pttrn, 'a] \<Rightarrow> letbind" (\<open>(2_ =/ _)\<close> 10)
+ "_bind" :: "[pttrn, 'a] \<Rightarrow> letbind" (\<open>(\<open>indent=2 notation=\<open>mixfix let binding\<close>\<close>_ =/ _)\<close> 10)
"" :: "letbind \<Rightarrow> letbinds" (\<open>_\<close>)
"_binds" :: "[letbind, letbinds] \<Rightarrow> letbinds" (\<open>_;/ _\<close>)
- "_Let" :: "[letbinds, 'a] \<Rightarrow> 'a" (\<open>(let (_)/ in (_))\<close> [0, 10] 10)
+ "_Let" :: "[letbinds, 'a] \<Rightarrow> 'a" (\<open>(\<open>notation=\<open>mixfix let expression\<close>\<close>let (_)/ in (_))\<close> [0, 10] 10)
syntax_consts
"_bind" "_binds" "_Let" \<rightleftharpoons> Let
translations
--- a/src/HOL/Hilbert_Choice.thy Mon Sep 23 15:01:10 2024 +0200
+++ b/src/HOL/Hilbert_Choice.thy Mon Sep 23 21:09:23 2024 +0200
@@ -17,11 +17,11 @@
where someI: "P x \<Longrightarrow> P (Eps P)"
syntax (epsilon)
- "_Eps" :: "pttrn \<Rightarrow> bool \<Rightarrow> 'a" (\<open>(3\<some>_./ _)\<close> [0, 10] 10)
+ "_Eps" :: "pttrn \<Rightarrow> bool \<Rightarrow> 'a" (\<open>(\<open>indent=3 notation=\<open>binder \<some>\<close>\<close>\<some>_./ _)\<close> [0, 10] 10)
syntax (input)
- "_Eps" :: "pttrn \<Rightarrow> bool \<Rightarrow> 'a" (\<open>(3@ _./ _)\<close> [0, 10] 10)
+ "_Eps" :: "pttrn \<Rightarrow> bool \<Rightarrow> 'a" (\<open>(\<open>indent=3 notation=\<open>binder @\<close>\<close>@ _./ _)\<close> [0, 10] 10)
syntax
- "_Eps" :: "pttrn \<Rightarrow> bool \<Rightarrow> 'a" (\<open>(3SOME _./ _)\<close> [0, 10] 10)
+ "_Eps" :: "pttrn \<Rightarrow> bool \<Rightarrow> 'a" (\<open>(\<open>indent=3 notation=\<open>binder SOME\<close>\<close>SOME _./ _)\<close> [0, 10] 10)
syntax_consts "_Eps" \<rightleftharpoons> Eps
--- a/src/HOL/Inductive.thy Mon Sep 23 15:01:10 2024 +0200
+++ b/src/HOL/Inductive.thy Mon Sep 23 21:09:23 2024 +0200
@@ -525,9 +525,9 @@
text \<open>Lambda-abstractions with pattern matching:\<close>
syntax (ASCII)
- "_lam_pats_syntax" :: "cases_syn \<Rightarrow> 'a \<Rightarrow> 'b" (\<open>(%_)\<close> 10)
+ "_lam_pats_syntax" :: "cases_syn \<Rightarrow> 'a \<Rightarrow> 'b" (\<open>(\<open>notation=abstraction\<close>%_)\<close> 10)
syntax
- "_lam_pats_syntax" :: "cases_syn \<Rightarrow> 'a \<Rightarrow> 'b" (\<open>(\<lambda>_)\<close> 10)
+ "_lam_pats_syntax" :: "cases_syn \<Rightarrow> 'a \<Rightarrow> 'b" (\<open>(\<open>notation=abstraction\<close>\<lambda>_)\<close> 10)
parse_translation \<open>
let
fun fun_tr ctxt [cs] =
--- a/src/HOL/Lattices_Big.thy Mon Sep 23 15:01:10 2024 +0200
+++ b/src/HOL/Lattices_Big.thy Mon Sep 23 21:09:23 2024 +0200
@@ -465,10 +465,10 @@
end
syntax
- "_MIN1" :: "pttrns \<Rightarrow> 'b \<Rightarrow> 'b" (\<open>(3MIN _./ _)\<close> [0, 10] 10)
- "_MIN" :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b \<Rightarrow> 'b" (\<open>(3MIN _\<in>_./ _)\<close> [0, 0, 10] 10)
- "_MAX1" :: "pttrns \<Rightarrow> 'b \<Rightarrow> 'b" (\<open>(3MAX _./ _)\<close> [0, 10] 10)
- "_MAX" :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b \<Rightarrow> 'b" (\<open>(3MAX _\<in>_./ _)\<close> [0, 0, 10] 10)
+ "_MIN1" :: "pttrns \<Rightarrow> 'b \<Rightarrow> 'b" (\<open>(\<open>indent=3 notation=\<open>binder MIN\<close>\<close>MIN _./ _)\<close> [0, 10] 10)
+ "_MIN" :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b \<Rightarrow> 'b" (\<open>(\<open>indent=3 notation=\<open>binder MIN\<close>\<close>MIN _\<in>_./ _)\<close> [0, 0, 10] 10)
+ "_MAX1" :: "pttrns \<Rightarrow> 'b \<Rightarrow> 'b" (\<open>(\<open>indent=3 notation=\<open>binder MAX\<close>\<close>MAX _./ _)\<close> [0, 10] 10)
+ "_MAX" :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b \<Rightarrow> 'b" (\<open>(\<open>indent=3 notation=\<open>binder MAX\<close>\<close>MAX _\<in>_./ _)\<close> [0, 0, 10] 10)
syntax_consts
"_MIN1" "_MIN" \<rightleftharpoons> Min and
@@ -923,7 +923,7 @@
syntax
"_arg_min" :: "('b \<Rightarrow> 'a) \<Rightarrow> pttrn \<Rightarrow> bool \<Rightarrow> 'b"
- (\<open>(3ARG'_MIN _ _./ _)\<close> [1000, 0, 10] 10)
+ (\<open>(\<open>indent=3 notation=\<open>binder ARG_MIN\<close>\<close>ARG'_MIN _ _./ _)\<close> [1000, 0, 10] 10)
syntax_consts
"_arg_min" \<rightleftharpoons> arg_min
translations
@@ -1034,7 +1034,7 @@
syntax
"_arg_max" :: "('b \<Rightarrow> 'a) \<Rightarrow> pttrn \<Rightarrow> bool \<Rightarrow> 'a"
- (\<open>(3ARG'_MAX _ _./ _)\<close> [1000, 0, 10] 10)
+ (\<open>(\<open>indent=3 notation=\<open>binder ARG_MAX\<close>\<close>ARG'_MAX _ _./ _)\<close> [1000, 0, 10] 10)
syntax_consts
"_arg_max" \<rightleftharpoons> arg_max
translations
--- a/src/HOL/List.thy Mon Sep 23 15:01:10 2024 +0200
+++ b/src/HOL/List.thy Mon Sep 23 21:09:23 2024 +0200
@@ -86,9 +86,9 @@
text \<open>Special input syntax for filter:\<close>
syntax (ASCII)
- "_filter" :: "[pttrn, 'a list, bool] => 'a list" (\<open>(1[_<-_./ _])\<close>)
+ "_filter" :: "[pttrn, 'a list, bool] => 'a list" (\<open>(\<open>indent=1 notation=\<open>mixfix filter\<close>\<close>[_<-_./ _])\<close>)
syntax
- "_filter" :: "[pttrn, 'a list, bool] => 'a list" (\<open>(1[_\<leftarrow>_ ./ _])\<close>)
+ "_filter" :: "[pttrn, 'a list, bool] => 'a list" (\<open>(\<open>indent=1 notation=\<open>mixfix filter\<close>\<close>[_\<leftarrow>_ ./ _])\<close>)
syntax_consts
"_filter" \<rightleftharpoons> filter
translations
@@ -135,7 +135,7 @@
nonterminal lupdbinds and lupdbind
syntax
- "_lupdbind":: "['a, 'a] => lupdbind" (\<open>(2_ :=/ _)\<close>)
+ "_lupdbind":: "['a, 'a] => lupdbind" (\<open>(\<open>indent=2 notation=\<open>mixfix list update\<close>\<close>_ :=/ _)\<close>)
"" :: "lupdbind => lupdbinds" (\<open>_\<close>)
"_lupdbinds" :: "[lupdbind, lupdbinds] => lupdbinds" (\<open>_,/ _\<close>)
"_LUpdate" :: "['a, lupdbinds] => 'a" (\<open>_/[(_)]\<close> [1000,0] 900)
@@ -175,7 +175,7 @@
"product_lists [] = [[]]" |
"product_lists (xs # xss) = concat (map (\<lambda>x. map (Cons x) (product_lists xss)) xs)"
-primrec upt :: "nat \<Rightarrow> nat \<Rightarrow> nat list" (\<open>(1[_..</_'])\<close>) where
+primrec upt :: "nat \<Rightarrow> nat \<Rightarrow> nat list" (\<open>(\<open>indent=1 notation=\<open>mixfix list interval\<close>\<close>[_..</_'])\<close>) where
upt_0: "[i..<0] = []" |
upt_Suc: "[i..<(Suc j)] = (if i \<le> j then [i..<j] @ [j] else [])"
@@ -3432,7 +3432,7 @@
subsubsection \<open>\<open>upto\<close>: interval-list on \<^typ>\<open>int\<close>\<close>
-function upto :: "int \<Rightarrow> int \<Rightarrow> int list" (\<open>(1[_../_])\<close>) where
+function upto :: "int \<Rightarrow> int \<Rightarrow> int list" (\<open>(\<open>indent=1 notation=\<open>mixfix list interval\<close>\<close>[_../_])\<close>) where
"upto i j = (if i \<le> j then i # [i+1..j] else [])"
by auto
termination
--- a/src/HOL/Main.thy Mon Sep 23 15:01:10 2024 +0200
+++ b/src/HOL/Main.thy Mon Sep 23 21:09:23 2024 +0200
@@ -77,10 +77,10 @@
Sup (\<open>\<Squnion> _\<close> [900] 900)
syntax
- "_INF1" :: "pttrns \<Rightarrow> 'b \<Rightarrow> 'b" (\<open>(3\<Sqinter>_./ _)\<close> [0, 10] 10)
- "_INF" :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b \<Rightarrow> 'b" (\<open>(3\<Sqinter>_\<in>_./ _)\<close> [0, 0, 10] 10)
- "_SUP1" :: "pttrns \<Rightarrow> 'b \<Rightarrow> 'b" (\<open>(3\<Squnion>_./ _)\<close> [0, 10] 10)
- "_SUP" :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b \<Rightarrow> 'b" (\<open>(3\<Squnion>_\<in>_./ _)\<close> [0, 0, 10] 10)
+ "_INF1" :: "pttrns \<Rightarrow> 'b \<Rightarrow> 'b" (\<open>(\<open>indent=3 notation=\<open>binder \<Sqinter>\<close>\<close>\<Sqinter>_./ _)\<close> [0, 10] 10)
+ "_INF" :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b \<Rightarrow> 'b" (\<open>(\<open>indent=3 notation=\<open>binder \<Sqinter>\<close>\<close>\<Sqinter>_\<in>_./ _)\<close> [0, 0, 10] 10)
+ "_SUP1" :: "pttrns \<Rightarrow> 'b \<Rightarrow> 'b" (\<open>(\<open>indent=3 notation=\<open>binder \<Squnion>\<close>\<close>\<Squnion>_./ _)\<close> [0, 10] 10)
+ "_SUP" :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b \<Rightarrow> 'b" (\<open>(\<open>indent=3 notation=\<open>binder \<Squnion>\<close>\<close>\<Squnion>_\<in>_./ _)\<close> [0, 0, 10] 10)
end
@@ -96,10 +96,10 @@
Sup (\<open>\<Squnion> _\<close> [900] 900)
no_syntax
- "_INF1" :: "pttrns \<Rightarrow> 'b \<Rightarrow> 'b" (\<open>(3\<Sqinter>_./ _)\<close> [0, 10] 10)
- "_INF" :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b \<Rightarrow> 'b" (\<open>(3\<Sqinter>_\<in>_./ _)\<close> [0, 0, 10] 10)
- "_SUP1" :: "pttrns \<Rightarrow> 'b \<Rightarrow> 'b" (\<open>(3\<Squnion>_./ _)\<close> [0, 10] 10)
- "_SUP" :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b \<Rightarrow> 'b" (\<open>(3\<Squnion>_\<in>_./ _)\<close> [0, 0, 10] 10)
+ "_INF1" :: "pttrns \<Rightarrow> 'b \<Rightarrow> 'b" (\<open>(\<open>indent=3 notation=\<open>binder \<Sqinter>\<close>\<close>\<Sqinter>_./ _)\<close> [0, 10] 10)
+ "_INF" :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b \<Rightarrow> 'b" (\<open>(\<open>indent=3 notation=\<open>binder \<Sqinter>\<close>\<close>\<Sqinter>_\<in>_./ _)\<close> [0, 0, 10] 10)
+ "_SUP1" :: "pttrns \<Rightarrow> 'b \<Rightarrow> 'b" (\<open>(\<open>indent=3 notation=\<open>binder \<Squnion>\<close>\<close>\<Squnion>_./ _)\<close> [0, 10] 10)
+ "_SUP" :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b \<Rightarrow> 'b" (\<open>(\<open>indent=3 notation=\<open>binder \<Squnion>\<close>\<close>\<Squnion>_\<in>_./ _)\<close> [0, 0, 10] 10)
end
--- a/src/HOL/Map.thy Mon Sep 23 15:01:10 2024 +0200
+++ b/src/HOL/Map.thy Mon Sep 23 21:09:23 2024 +0200
@@ -61,7 +61,7 @@
"" :: "maplet \<Rightarrow> updbind" (\<open>_\<close>)
"" :: "maplet \<Rightarrow> maplets" (\<open>_\<close>)
"_Maplets" :: "[maplet, maplets] \<Rightarrow> maplets" (\<open>_,/ _\<close>)
- "_Map" :: "maplets \<Rightarrow> 'a \<rightharpoonup> 'b" (\<open>(1[_])\<close>)
+ "_Map" :: "maplets \<Rightarrow> 'a \<rightharpoonup> 'b" (\<open>(\<open>indent=1 notation=\<open>mixfix maplets\<close>\<close>[_])\<close>)
(* Syntax forbids \<open>[\<dots>, x := y, \<dots>]\<close> by introducing \<open>maplets\<close> in addition to \<open>updbinds\<close> *)
syntax (ASCII)
--- a/src/HOL/Orderings.thy Mon Sep 23 15:01:10 2024 +0200
+++ b/src/HOL/Orderings.thy Mon Sep 23 21:09:23 2024 +0200
@@ -179,9 +179,9 @@
notation
less_eq (\<open>'(\<le>')\<close>) and
- less_eq (\<open>(_/ \<le> _)\<close> [51, 51] 50) and
+ less_eq (\<open>(\<open>notation=\<open>infix \<le>\<close>\<close>_/ \<le> _)\<close> [51, 51] 50) and
less (\<open>'(<')\<close>) and
- less (\<open>(_/ < _)\<close> [51, 51] 50)
+ less (\<open>(\<open>notation=\<open>infix <\<close>\<close>_/ < _)\<close> [51, 51] 50)
abbreviation (input)
greater_eq (infix \<open>\<ge>\<close> 50)
@@ -193,7 +193,7 @@
notation (ASCII)
less_eq (\<open>'(<=')\<close>) and
- less_eq (\<open>(_/ <= _)\<close> [51, 51] 50)
+ less_eq (\<open>(\<open>notation=\<open>infix <=\<close>\<close>_/ <= _)\<close> [51, 51] 50)
notation (input)
greater_eq (infix \<open>>=\<close> 50)
@@ -710,40 +710,40 @@
subsection \<open>Bounded quantifiers\<close>
syntax (ASCII)
- "_All_less" :: "[idt, 'a, bool] => bool" (\<open>(3ALL _<_./ _)\<close> [0, 0, 10] 10)
- "_Ex_less" :: "[idt, 'a, bool] => bool" (\<open>(3EX _<_./ _)\<close> [0, 0, 10] 10)
- "_All_less_eq" :: "[idt, 'a, bool] => bool" (\<open>(3ALL _<=_./ _)\<close> [0, 0, 10] 10)
- "_Ex_less_eq" :: "[idt, 'a, bool] => bool" (\<open>(3EX _<=_./ _)\<close> [0, 0, 10] 10)
+ "_All_less" :: "[idt, 'a, bool] => bool" (\<open>(\<open>indent=3 notation=\<open>binder ALL\<close>\<close>ALL _<_./ _)\<close> [0, 0, 10] 10)
+ "_Ex_less" :: "[idt, 'a, bool] => bool" (\<open>(\<open>indent=3 notation=\<open>binder EX\<close>\<close>EX _<_./ _)\<close> [0, 0, 10] 10)
+ "_All_less_eq" :: "[idt, 'a, bool] => bool" (\<open>(\<open>indent=3 notation=\<open>binder ALL\<close>\<close>ALL _<=_./ _)\<close> [0, 0, 10] 10)
+ "_Ex_less_eq" :: "[idt, 'a, bool] => bool" (\<open>(\<open>indent=3 notation=\<open>binder EX\<close>\<close>EX _<=_./ _)\<close> [0, 0, 10] 10)
- "_All_greater" :: "[idt, 'a, bool] => bool" (\<open>(3ALL _>_./ _)\<close> [0, 0, 10] 10)
- "_Ex_greater" :: "[idt, 'a, bool] => bool" (\<open>(3EX _>_./ _)\<close> [0, 0, 10] 10)
- "_All_greater_eq" :: "[idt, 'a, bool] => bool" (\<open>(3ALL _>=_./ _)\<close> [0, 0, 10] 10)
- "_Ex_greater_eq" :: "[idt, 'a, bool] => bool" (\<open>(3EX _>=_./ _)\<close> [0, 0, 10] 10)
+ "_All_greater" :: "[idt, 'a, bool] => bool" (\<open>(\<open>indent=3 notation=\<open>binder ALL\<close>\<close>ALL _>_./ _)\<close> [0, 0, 10] 10)
+ "_Ex_greater" :: "[idt, 'a, bool] => bool" (\<open>(\<open>indent=3 notation=\<open>binder EX\<close>\<close>EX _>_./ _)\<close> [0, 0, 10] 10)
+ "_All_greater_eq" :: "[idt, 'a, bool] => bool" (\<open>(\<open>indent=3 notation=\<open>binder ALL\<close>\<close>ALL _>=_./ _)\<close> [0, 0, 10] 10)
+ "_Ex_greater_eq" :: "[idt, 'a, bool] => bool" (\<open>(\<open>indent=3 notation=\<open>binder EX\<close>\<close>EX _>=_./ _)\<close> [0, 0, 10] 10)
- "_All_neq" :: "[idt, 'a, bool] => bool" (\<open>(3ALL _~=_./ _)\<close> [0, 0, 10] 10)
- "_Ex_neq" :: "[idt, 'a, bool] => bool" (\<open>(3EX _~=_./ _)\<close> [0, 0, 10] 10)
+ "_All_neq" :: "[idt, 'a, bool] => bool" (\<open>(\<open>indent=3 notation=\<open>binder ALL\<close>\<close>ALL _~=_./ _)\<close> [0, 0, 10] 10)
+ "_Ex_neq" :: "[idt, 'a, bool] => bool" (\<open>(\<open>indent=3 notation=\<open>binder EX\<close>\<close>EX _~=_./ _)\<close> [0, 0, 10] 10)
syntax
- "_All_less" :: "[idt, 'a, bool] => bool" (\<open>(3\<forall>_<_./ _)\<close> [0, 0, 10] 10)
- "_Ex_less" :: "[idt, 'a, bool] => bool" (\<open>(3\<exists>_<_./ _)\<close> [0, 0, 10] 10)
- "_All_less_eq" :: "[idt, 'a, bool] => bool" (\<open>(3\<forall>_\<le>_./ _)\<close> [0, 0, 10] 10)
- "_Ex_less_eq" :: "[idt, 'a, bool] => bool" (\<open>(3\<exists>_\<le>_./ _)\<close> [0, 0, 10] 10)
+ "_All_less" :: "[idt, 'a, bool] => bool" (\<open>(\<open>indent=3 notation=\<open>binder \<forall>\<close>\<close>\<forall>_<_./ _)\<close> [0, 0, 10] 10)
+ "_Ex_less" :: "[idt, 'a, bool] => bool" (\<open>(\<open>indent=3 notation=\<open>binder \<exists>\<close>\<close>\<exists>_<_./ _)\<close> [0, 0, 10] 10)
+ "_All_less_eq" :: "[idt, 'a, bool] => bool" (\<open>(\<open>indent=3 notation=\<open>binder \<forall>\<close>\<close>\<forall>_\<le>_./ _)\<close> [0, 0, 10] 10)
+ "_Ex_less_eq" :: "[idt, 'a, bool] => bool" (\<open>(\<open>indent=3 notation=\<open>binder \<exists>\<close>\<close>\<exists>_\<le>_./ _)\<close> [0, 0, 10] 10)
- "_All_greater" :: "[idt, 'a, bool] => bool" (\<open>(3\<forall>_>_./ _)\<close> [0, 0, 10] 10)
- "_Ex_greater" :: "[idt, 'a, bool] => bool" (\<open>(3\<exists>_>_./ _)\<close> [0, 0, 10] 10)
- "_All_greater_eq" :: "[idt, 'a, bool] => bool" (\<open>(3\<forall>_\<ge>_./ _)\<close> [0, 0, 10] 10)
- "_Ex_greater_eq" :: "[idt, 'a, bool] => bool" (\<open>(3\<exists>_\<ge>_./ _)\<close> [0, 0, 10] 10)
+ "_All_greater" :: "[idt, 'a, bool] => bool" (\<open>(\<open>indent=3 notation=\<open>binder \<forall>\<close>\<close>\<forall>_>_./ _)\<close> [0, 0, 10] 10)
+ "_Ex_greater" :: "[idt, 'a, bool] => bool" (\<open>(\<open>indent=3 notation=\<open>binder \<exists>\<close>\<close>\<exists>_>_./ _)\<close> [0, 0, 10] 10)
+ "_All_greater_eq" :: "[idt, 'a, bool] => bool" (\<open>(\<open>indent=3 notation=\<open>binder \<forall>\<close>\<close>\<forall>_\<ge>_./ _)\<close> [0, 0, 10] 10)
+ "_Ex_greater_eq" :: "[idt, 'a, bool] => bool" (\<open>(\<open>indent=3 notation=\<open>binder \<exists>\<close>\<close>\<exists>_\<ge>_./ _)\<close> [0, 0, 10] 10)
- "_All_neq" :: "[idt, 'a, bool] => bool" (\<open>(3\<forall>_\<noteq>_./ _)\<close> [0, 0, 10] 10)
- "_Ex_neq" :: "[idt, 'a, bool] => bool" (\<open>(3\<exists>_\<noteq>_./ _)\<close> [0, 0, 10] 10)
+ "_All_neq" :: "[idt, 'a, bool] => bool" (\<open>(\<open>indent=3 notation=\<open>binder \<forall>\<close>\<close>\<forall>_\<noteq>_./ _)\<close> [0, 0, 10] 10)
+ "_Ex_neq" :: "[idt, 'a, bool] => bool" (\<open>(\<open>indent=3 notation=\<open>binder \<exists>\<close>\<close>\<exists>_\<noteq>_./ _)\<close> [0, 0, 10] 10)
syntax (input)
- "_All_less" :: "[idt, 'a, bool] => bool" (\<open>(3! _<_./ _)\<close> [0, 0, 10] 10)
- "_Ex_less" :: "[idt, 'a, bool] => bool" (\<open>(3? _<_./ _)\<close> [0, 0, 10] 10)
- "_All_less_eq" :: "[idt, 'a, bool] => bool" (\<open>(3! _<=_./ _)\<close> [0, 0, 10] 10)
- "_Ex_less_eq" :: "[idt, 'a, bool] => bool" (\<open>(3? _<=_./ _)\<close> [0, 0, 10] 10)
- "_All_neq" :: "[idt, 'a, bool] => bool" (\<open>(3! _~=_./ _)\<close> [0, 0, 10] 10)
- "_Ex_neq" :: "[idt, 'a, bool] => bool" (\<open>(3? _~=_./ _)\<close> [0, 0, 10] 10)
+ "_All_less" :: "[idt, 'a, bool] => bool" (\<open>(\<open>indent=3 notation=\<open>binder !\<close>\<close>! _<_./ _)\<close> [0, 0, 10] 10)
+ "_Ex_less" :: "[idt, 'a, bool] => bool" (\<open>(\<open>indent=3 notation=\<open>binder ?\<close>\<close>? _<_./ _)\<close> [0, 0, 10] 10)
+ "_All_less_eq" :: "[idt, 'a, bool] => bool" (\<open>(\<open>indent=3 notation=\<open>binder !\<close>\<close>! _<=_./ _)\<close> [0, 0, 10] 10)
+ "_Ex_less_eq" :: "[idt, 'a, bool] => bool" (\<open>(\<open>indent=3 notation=\<open>binder ?\<close>\<close>? _<=_./ _)\<close> [0, 0, 10] 10)
+ "_All_neq" :: "[idt, 'a, bool] => bool" (\<open>(\<open>indent=3 notation=\<open>binder !\<close>\<close>! _~=_./ _)\<close> [0, 0, 10] 10)
+ "_Ex_neq" :: "[idt, 'a, bool] => bool" (\<open>(\<open>indent=3 notation=\<open>binder ?\<close>\<close>? _~=_./ _)\<close> [0, 0, 10] 10)
syntax_consts
"_All_less" "_All_less_eq" "_All_greater" "_All_greater_eq" "_All_neq" \<rightleftharpoons> All and
--- a/src/HOL/Power.thy Mon Sep 23 15:01:10 2024 +0200
+++ b/src/HOL/Power.thy Mon Sep 23 21:09:23 2024 +0200
@@ -23,7 +23,7 @@
power (\<open>(_\<^bsup>_\<^esup>)\<close> [1000] 1000)
text \<open>Special syntax for squares.\<close>
-abbreviation power2 :: "'a \<Rightarrow> 'a" (\<open>(_\<^sup>2)\<close> [1000] 999)
+abbreviation power2 :: "'a \<Rightarrow> 'a" (\<open>(\<open>notation=\<open>postfix 2\<close>\<close>_\<^sup>2)\<close> [1000] 999)
where "x\<^sup>2 \<equiv> x ^ 2"
end
--- a/src/HOL/Product_Type.thy Mon Sep 23 15:01:10 2024 +0200
+++ b/src/HOL/Product_Type.thy Mon Sep 23 21:09:23 2024 +0200
@@ -214,7 +214,7 @@
definition "prod = {f. \<exists>a b. f = Pair_Rep (a::'a) (b::'b)}"
-typedef ('a, 'b) prod (\<open>(_ \<times>/ _)\<close> [21, 20] 20) = "prod :: ('a \<Rightarrow> 'b \<Rightarrow> bool) set"
+typedef ('a, 'b) prod (\<open>(\<open>notation=\<open>infix \<times>\<close>\<close>_ \<times>/ _)\<close> [21, 20] 20) = "prod :: ('a \<Rightarrow> 'b \<Rightarrow> bool) set"
unfolding prod_def by auto
type_notation (ASCII)
@@ -286,7 +286,7 @@
nonterminal tuple_args and patterns
syntax
- "_tuple" :: "'a \<Rightarrow> tuple_args \<Rightarrow> 'a \<times> 'b" (\<open>(1'(_,/ _'))\<close>)
+ "_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>)
@@ -1013,7 +1013,8 @@
end
syntax
- "_Sigma" :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b set \<Rightarrow> ('a \<times> 'b) set" (\<open>(3SIGMA _:_./ _)\<close> [0, 0, 10] 10)
+ "_Sigma" :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b set \<Rightarrow> ('a \<times> 'b) set"
+ (\<open>(\<open>indent=3 notation=\<open>binder SIGMA\<close>\<close>SIGMA _:_./ _)\<close> [0, 0, 10] 10)
syntax_consts
"_Sigma" \<rightleftharpoons> Sigma
translations
--- a/src/HOL/Record.thy Mon Sep 23 15:01:10 2024 +0200
+++ b/src/HOL/Record.thy Mon Sep 23 21:09:23 2024 +0200
@@ -426,29 +426,29 @@
"_constify" :: "id => ident" (\<open>_\<close>)
"_constify" :: "longid => ident" (\<open>_\<close>)
- "_field_type" :: "ident => type => field_type" (\<open>(2_ ::/ _)\<close>)
+ "_field_type" :: "ident => type => field_type" (\<open>(\<open>indent=2 notation=\<open>infix field type\<close>\<close>_ ::/ _)\<close>)
"" :: "field_type => field_types" (\<open>_\<close>)
"_field_types" :: "field_type => field_types => field_types" (\<open>_,/ _\<close>)
- "_record_type" :: "field_types => type" (\<open>(3\<lparr>_\<rparr>)\<close>)
- "_record_type_scheme" :: "field_types => type => type" (\<open>(3\<lparr>_,/ (2\<dots> ::/ _)\<rparr>)\<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>)
- "_field" :: "ident => 'a => field" (\<open>(2_ =/ _)\<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>(3\<lparr>_\<rparr>)\<close>)
- "_record_scheme" :: "fields => 'a => 'a" (\<open>(3\<lparr>_,/ (2\<dots> =/ _)\<rparr>)\<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>)
- "_field_update" :: "ident => 'a => field_update" (\<open>(2_ :=/ _)\<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>_/(3\<lparr>_\<rparr>)\<close> [900, 0] 900)
+ "_record_update" :: "'a => field_updates => 'b" (\<open>_/(\<open>indent=3 notation=\<open>mixfix record update\<close>\<close>\<lparr>_\<rparr>)\<close> [900, 0] 900)
syntax (ASCII)
- "_record_type" :: "field_types => type" (\<open>(3'(| _ |'))\<close>)
- "_record_type_scheme" :: "field_types => type => type" (\<open>(3'(| _,/ (2... ::/ _) |'))\<close>)
- "_record" :: "fields => 'a" (\<open>(3'(| _ |'))\<close>)
- "_record_scheme" :: "fields => 'a => 'a" (\<open>(3'(| _,/ (2... =/ _) |'))\<close>)
- "_record_update" :: "'a => field_updates => 'b" (\<open>_/(3'(| _ |'))\<close> [900, 0] 900)
+ "_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" :: "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)
subsection \<open>Record package\<close>
--- a/src/HOL/Relation.thy Mon Sep 23 15:01:10 2024 +0200
+++ b/src/HOL/Relation.thy Mon Sep 23 21:09:23 2024 +0200
@@ -1074,15 +1074,15 @@
subsubsection \<open>Converse\<close>
-inductive_set converse :: "('a \<times> 'b) set \<Rightarrow> ('b \<times> 'a) set" (\<open>(_\<inverse>)\<close> [1000] 999)
+inductive_set converse :: "('a \<times> 'b) set \<Rightarrow> ('b \<times> 'a) set" (\<open>(\<open>notation=\<open>postfix -1\<close>\<close>_\<inverse>)\<close> [1000] 999)
for r :: "('a \<times> 'b) set"
where "(a, b) \<in> r \<Longrightarrow> (b, a) \<in> r\<inverse>"
-notation conversep (\<open>(_\<inverse>\<inverse>)\<close> [1000] 1000)
+notation conversep (\<open>(\<open>notation=\<open>postfix -1-1\<close>\<close>_\<inverse>\<inverse>)\<close> [1000] 1000)
notation (ASCII)
- converse (\<open>(_^-1)\<close> [1000] 999) and
- conversep (\<open>(_^--1)\<close> [1000] 1000)
+ converse (\<open>(\<open>notation=\<open>postfix -1\<close>\<close>_^-1)\<close> [1000] 999) and
+ conversep (\<open>(\<open>notation=\<open>postfix -1-1\<close>\<close>_^--1)\<close> [1000] 1000)
lemma converseI [sym]: "(a, b) \<in> r \<Longrightarrow> (b, a) \<in> r\<inverse>"
by (fact converse.intros)
--- a/src/HOL/Set.thy Mon Sep 23 15:01:10 2024 +0200
+++ b/src/HOL/Set.thy Mon Sep 23 21:09:23 2024 +0200
@@ -21,34 +21,34 @@
notation
member (\<open>'(\<in>')\<close>) and
- member (\<open>(_/ \<in> _)\<close> [51, 51] 50)
+ member (\<open>(\<open>notation=\<open>infix \<in>\<close>\<close>_/ \<in> _)\<close> [51, 51] 50)
abbreviation not_member
where "not_member x A \<equiv> \<not> (x \<in> A)" \<comment> \<open>non-membership\<close>
notation
not_member (\<open>'(\<notin>')\<close>) and
- not_member (\<open>(_/ \<notin> _)\<close> [51, 51] 50)
+ not_member (\<open>(\<open>notation=\<open>infix \<notin>\<close>\<close>_/ \<notin> _)\<close> [51, 51] 50)
notation (ASCII)
member (\<open>'(:')\<close>) and
- member (\<open>(_/ : _)\<close> [51, 51] 50) and
+ member (\<open>(\<open>notation=\<open>infix :\<close>\<close>_/ : _)\<close> [51, 51] 50) and
not_member (\<open>'(~:')\<close>) and
- not_member (\<open>(_/ ~: _)\<close> [51, 51] 50)
+ not_member (\<open>(\<open>notation=\<open>infix ~:\<close>\<close>_/ ~: _)\<close> [51, 51] 50)
text \<open>Set comprehensions\<close>
syntax
- "_Coll" :: "pttrn \<Rightarrow> bool \<Rightarrow> 'a set" (\<open>(1{_./ _})\<close>)
+ "_Coll" :: "pttrn \<Rightarrow> bool \<Rightarrow> 'a set" (\<open>(\<open>indent=1 notation=\<open>mixfix Collect\<close>\<close>{_./ _})\<close>)
syntax_consts
"_Coll" \<rightleftharpoons> Collect
translations
"{x. P}" \<rightleftharpoons> "CONST Collect (\<lambda>x. P)"
syntax (ASCII)
- "_Collect" :: "pttrn \<Rightarrow> 'a set \<Rightarrow> bool \<Rightarrow> 'a set" (\<open>(1{(_/: _)./ _})\<close>)
+ "_Collect" :: "pttrn \<Rightarrow> 'a set \<Rightarrow> bool \<Rightarrow> 'a set" (\<open>(\<open>indent=1 notation=\<open>mixfix Collect\<close>\<close>{(_/: _)./ _})\<close>)
syntax
- "_Collect" :: "pttrn \<Rightarrow> 'a set \<Rightarrow> bool \<Rightarrow> 'a set" (\<open>(1{(_/ \<in> _)./ _})\<close>)
+ "_Collect" :: "pttrn \<Rightarrow> 'a set \<Rightarrow> bool \<Rightarrow> 'a set" (\<open>(\<open>indent=1 notation=\<open>mixfix Collect\<close>\<close>{(_/ \<in> _)./ _})\<close>)
syntax_consts
"_Collect" \<rightleftharpoons> Collect
translations
@@ -165,9 +165,9 @@
notation
subset (\<open>'(\<subset>')\<close>) and
- subset (\<open>(_/ \<subset> _)\<close> [51, 51] 50) and
+ subset (\<open>(\<open>notation=\<open>infix \<subset>\<close>\<close>_/ \<subset> _)\<close> [51, 51] 50) and
subset_eq (\<open>'(\<subseteq>')\<close>) and
- subset_eq (\<open>(_/ \<subseteq> _)\<close> [51, 51] 50)
+ subset_eq (\<open>(\<open>notation=\<open>infix \<subseteq>\<close>\<close>_/ \<subseteq> _)\<close> [51, 51] 50)
abbreviation (input)
supset :: "'a set \<Rightarrow> 'a set \<Rightarrow> bool" where
@@ -179,15 +179,15 @@
notation
supset (\<open>'(\<supset>')\<close>) and
- supset (\<open>(_/ \<supset> _)\<close> [51, 51] 50) and
+ supset (\<open>(\<open>notation=\<open>infix \<supset>\<close>\<close>_/ \<supset> _)\<close> [51, 51] 50) and
supset_eq (\<open>'(\<supseteq>')\<close>) and
- supset_eq (\<open>(_/ \<supseteq> _)\<close> [51, 51] 50)
+ supset_eq (\<open>(\<open>notation=\<open>infix \<supseteq>\<close>\<close>_/ \<supseteq> _)\<close> [51, 51] 50)
notation (ASCII output)
subset (\<open>'(<')\<close>) and
- subset (\<open>(_/ < _)\<close> [51, 51] 50) and
+ subset (\<open>(\<open>notation=\<open>infix <\<close>\<close>_/ < _)\<close> [51, 51] 50) and
subset_eq (\<open>'(<=')\<close>) and
- subset_eq (\<open>(_/ <= _)\<close> [51, 51] 50)
+ subset_eq (\<open>(\<open>notation=\<open>infix <=\<close>\<close>_/ <= _)\<close> [51, 51] 50)
definition Ball :: "'a set \<Rightarrow> ('a \<Rightarrow> bool) \<Rightarrow> bool"
where "Ball A P \<longleftrightarrow> (\<forall>x. x \<in> A \<longrightarrow> P x)" \<comment> \<open>bounded universal quantifiers\<close>
@@ -196,21 +196,21 @@
where "Bex A P \<longleftrightarrow> (\<exists>x. x \<in> A \<and> P x)" \<comment> \<open>bounded existential quantifiers\<close>
syntax (ASCII)
- "_Ball" :: "pttrn \<Rightarrow> 'a set \<Rightarrow> bool \<Rightarrow> bool" (\<open>(3ALL (_/:_)./ _)\<close> [0, 0, 10] 10)
- "_Bex" :: "pttrn \<Rightarrow> 'a set \<Rightarrow> bool \<Rightarrow> bool" (\<open>(3EX (_/:_)./ _)\<close> [0, 0, 10] 10)
- "_Bex1" :: "pttrn \<Rightarrow> 'a set \<Rightarrow> bool \<Rightarrow> bool" (\<open>(3EX! (_/:_)./ _)\<close> [0, 0, 10] 10)
- "_Bleast" :: "id \<Rightarrow> 'a set \<Rightarrow> bool \<Rightarrow> 'a" (\<open>(3LEAST (_/:_)./ _)\<close> [0, 0, 10] 10)
+ "_Ball" :: "pttrn \<Rightarrow> 'a set \<Rightarrow> bool \<Rightarrow> bool" (\<open>(\<open>indent=3 notation=\<open>binder ALL :\<close>\<close>ALL (_/:_)./ _)\<close> [0, 0, 10] 10)
+ "_Bex" :: "pttrn \<Rightarrow> 'a set \<Rightarrow> bool \<Rightarrow> bool" (\<open>(\<open>indent=3 notation=\<open>binder EX :\<close>\<close>EX (_/:_)./ _)\<close> [0, 0, 10] 10)
+ "_Bex1" :: "pttrn \<Rightarrow> 'a set \<Rightarrow> bool \<Rightarrow> bool" (\<open>(\<open>indent=3 notation=\<open>binder EX! :\<close>\<close>EX! (_/:_)./ _)\<close> [0, 0, 10] 10)
+ "_Bleast" :: "id \<Rightarrow> 'a set \<Rightarrow> bool \<Rightarrow> 'a" (\<open>(\<open>indent=3 notation=\<open>binder LEAST :\<close>\<close>LEAST (_/:_)./ _)\<close> [0, 0, 10] 10)
syntax (input)
- "_Ball" :: "pttrn \<Rightarrow> 'a set \<Rightarrow> bool \<Rightarrow> bool" (\<open>(3! (_/:_)./ _)\<close> [0, 0, 10] 10)
- "_Bex" :: "pttrn \<Rightarrow> 'a set \<Rightarrow> bool \<Rightarrow> bool" (\<open>(3? (_/:_)./ _)\<close> [0, 0, 10] 10)
- "_Bex1" :: "pttrn \<Rightarrow> 'a set \<Rightarrow> bool \<Rightarrow> bool" (\<open>(3?! (_/:_)./ _)\<close> [0, 0, 10] 10)
+ "_Ball" :: "pttrn \<Rightarrow> 'a set \<Rightarrow> bool \<Rightarrow> bool" (\<open>(\<open>indent=3 notation=\<open>binder ! :\<close>\<close>! (_/:_)./ _)\<close> [0, 0, 10] 10)
+ "_Bex" :: "pttrn \<Rightarrow> 'a set \<Rightarrow> bool \<Rightarrow> bool" (\<open>(\<open>indent=3 notation=\<open>binder ? :\<close>\<close>? (_/:_)./ _)\<close> [0, 0, 10] 10)
+ "_Bex1" :: "pttrn \<Rightarrow> 'a set \<Rightarrow> bool \<Rightarrow> bool" (\<open>(\<open>indent=3 notation=\<open>binder ?! :\<close>\<close>?! (_/:_)./ _)\<close> [0, 0, 10] 10)
syntax
- "_Ball" :: "pttrn \<Rightarrow> 'a set \<Rightarrow> bool \<Rightarrow> bool" (\<open>(3\<forall>(_/\<in>_)./ _)\<close> [0, 0, 10] 10)
- "_Bex" :: "pttrn \<Rightarrow> 'a set \<Rightarrow> bool \<Rightarrow> bool" (\<open>(3\<exists>(_/\<in>_)./ _)\<close> [0, 0, 10] 10)
- "_Bex1" :: "pttrn \<Rightarrow> 'a set \<Rightarrow> bool \<Rightarrow> bool" (\<open>(3\<exists>!(_/\<in>_)./ _)\<close> [0, 0, 10] 10)
- "_Bleast" :: "id \<Rightarrow> 'a set \<Rightarrow> bool \<Rightarrow> 'a" (\<open>(3LEAST(_/\<in>_)./ _)\<close> [0, 0, 10] 10)
+ "_Ball" :: "pttrn \<Rightarrow> 'a set \<Rightarrow> bool \<Rightarrow> bool" (\<open>(\<open>indent=3 notation=\<open>binder \<forall>\<close>\<close>\<forall>(_/\<in>_)./ _)\<close> [0, 0, 10] 10)
+ "_Bex" :: "pttrn \<Rightarrow> 'a set \<Rightarrow> bool \<Rightarrow> bool" (\<open>(\<open>indent=3 notation=\<open>binder \<exists>\<close>\<close>\<exists>(_/\<in>_)./ _)\<close> [0, 0, 10] 10)
+ "_Bex1" :: "pttrn \<Rightarrow> 'a set \<Rightarrow> bool \<Rightarrow> bool" (\<open>(\<open>indent=3 notation=\<open>binder \<exists>!\<close>\<close>\<exists>!(_/\<in>_)./ _)\<close> [0, 0, 10] 10)
+ "_Bleast" :: "id \<Rightarrow> 'a set \<Rightarrow> bool \<Rightarrow> 'a" (\<open>(\<open>indent=3 notation=\<open>binder LEAST\<close>\<close>LEAST(_/\<in>_)./ _)\<close> [0, 0, 10] 10)
syntax_consts
"_Ball" \<rightleftharpoons> Ball and
@@ -225,18 +225,18 @@
"LEAST x:A. P" \<rightharpoonup> "LEAST x. x \<in> A \<and> P"
syntax (ASCII output)
- "_setlessAll" :: "[idt, 'a, bool] \<Rightarrow> bool" (\<open>(3ALL _<_./ _)\<close> [0, 0, 10] 10)
- "_setlessEx" :: "[idt, 'a, bool] \<Rightarrow> bool" (\<open>(3EX _<_./ _)\<close> [0, 0, 10] 10)
- "_setleAll" :: "[idt, 'a, bool] \<Rightarrow> bool" (\<open>(3ALL _<=_./ _)\<close> [0, 0, 10] 10)
- "_setleEx" :: "[idt, 'a, bool] \<Rightarrow> bool" (\<open>(3EX _<=_./ _)\<close> [0, 0, 10] 10)
- "_setleEx1" :: "[idt, 'a, bool] \<Rightarrow> bool" (\<open>(3EX! _<=_./ _)\<close> [0, 0, 10] 10)
+ "_setlessAll" :: "[idt, 'a, bool] \<Rightarrow> bool" (\<open>(\<open>indent=3 notation=\<open>binder ALL\<close>\<close>ALL _<_./ _)\<close> [0, 0, 10] 10)
+ "_setlessEx" :: "[idt, 'a, bool] \<Rightarrow> bool" (\<open>(\<open>indent=3 notation=\<open>binder EX\<close>\<close>EX _<_./ _)\<close> [0, 0, 10] 10)
+ "_setleAll" :: "[idt, 'a, bool] \<Rightarrow> bool" (\<open>(\<open>indent=3 notation=\<open>binder ALL\<close>\<close>ALL _<=_./ _)\<close> [0, 0, 10] 10)
+ "_setleEx" :: "[idt, 'a, bool] \<Rightarrow> bool" (\<open>(\<open>indent=3 notation=\<open>binder EX\<close>\<close>EX _<=_./ _)\<close> [0, 0, 10] 10)
+ "_setleEx1" :: "[idt, 'a, bool] \<Rightarrow> bool" (\<open>(\<open>indent=3 notation=\<open>binder EX!\<close>\<close>EX! _<=_./ _)\<close> [0, 0, 10] 10)
syntax
- "_setlessAll" :: "[idt, 'a, bool] \<Rightarrow> bool" (\<open>(3\<forall>_\<subset>_./ _)\<close> [0, 0, 10] 10)
- "_setlessEx" :: "[idt, 'a, bool] \<Rightarrow> bool" (\<open>(3\<exists>_\<subset>_./ _)\<close> [0, 0, 10] 10)
- "_setleAll" :: "[idt, 'a, bool] \<Rightarrow> bool" (\<open>(3\<forall>_\<subseteq>_./ _)\<close> [0, 0, 10] 10)
- "_setleEx" :: "[idt, 'a, bool] \<Rightarrow> bool" (\<open>(3\<exists>_\<subseteq>_./ _)\<close> [0, 0, 10] 10)
- "_setleEx1" :: "[idt, 'a, bool] \<Rightarrow> bool" (\<open>(3\<exists>!_\<subseteq>_./ _)\<close> [0, 0, 10] 10)
+ "_setlessAll" :: "[idt, 'a, bool] \<Rightarrow> bool" (\<open>(\<open>indent=3 notation=\<open>binder \<forall>\<close>\<close>\<forall>_\<subset>_./ _)\<close> [0, 0, 10] 10)
+ "_setlessEx" :: "[idt, 'a, bool] \<Rightarrow> bool" (\<open>(\<open>indent=3 notation=\<open>binder \<exists>\<close>\<close>\<exists>_\<subset>_./ _)\<close> [0, 0, 10] 10)
+ "_setleAll" :: "[idt, 'a, bool] \<Rightarrow> bool" (\<open>(\<open>indent=3 notation=\<open>binder \<forall>\<close>\<close>\<forall>_\<subseteq>_./ _)\<close> [0, 0, 10] 10)
+ "_setleEx" :: "[idt, 'a, bool] \<Rightarrow> bool" (\<open>(\<open>indent=3 notation=\<open>binder \<exists>\<close>\<close>\<exists>_\<subseteq>_./ _)\<close> [0, 0, 10] 10)
+ "_setleEx1" :: "[idt, 'a, bool] \<Rightarrow> bool" (\<open>(\<open>indent=3 notation=\<open>binder \<exists>!\<close>\<close>\<exists>!_\<subseteq>_./ _)\<close> [0, 0, 10] 10)
syntax_consts
"_setlessAll" "_setleAll" \<rightleftharpoons> All and
@@ -291,7 +291,8 @@
\<close>
syntax
- "_Setcompr" :: "'a \<Rightarrow> idts \<Rightarrow> bool \<Rightarrow> 'a set" (\<open>(1{_ |/_./ _})\<close>)
+ "_Setcompr" :: "'a \<Rightarrow> idts \<Rightarrow> bool \<Rightarrow> 'a set"
+ (\<open>(\<open>indent=1 notation=\<open>mixfix set comprehension\<close>\<close>{_ |/_./ _})\<close>)
syntax_consts
"_Setcompr" \<rightleftharpoons> Collect
--- a/src/HOL/Set_Interval.thy Mon Sep 23 15:01:10 2024 +0200
+++ b/src/HOL/Set_Interval.thy Mon Sep 23 21:09:23 2024 +0200
@@ -29,35 +29,35 @@
begin
definition
- lessThan :: "'a => 'a set" (\<open>(1{..<_})\<close>) where
+ lessThan :: "'a => 'a set" (\<open>(\<open>indent=1 notation=\<open>mixfix set interval\<close>\<close>{..<_})\<close>) where
"{..<u} == {x. x < u}"
definition
- atMost :: "'a => 'a set" (\<open>(1{.._})\<close>) where
+ atMost :: "'a => 'a set" (\<open>(\<open>indent=1 notation=\<open>mixfix set interval\<close>\<close>{.._})\<close>) where
"{..u} == {x. x \<le> u}"
definition
- greaterThan :: "'a => 'a set" (\<open>(1{_<..})\<close>) where
+ greaterThan :: "'a => 'a set" (\<open>(\<open>indent=1 notation=\<open>mixfix set interval\<close>\<close>{_<..})\<close>) where
"{l<..} == {x. l<x}"
definition
- atLeast :: "'a => 'a set" (\<open>(1{_..})\<close>) where
+ atLeast :: "'a => 'a set" (\<open>(\<open>indent=1 notation=\<open>mixfix set interval\<close>\<close>{_..})\<close>) where
"{l..} == {x. l\<le>x}"
definition
- greaterThanLessThan :: "'a => 'a => 'a set" (\<open>(1{_<..<_})\<close>) where
+ greaterThanLessThan :: "'a => 'a => 'a set" (\<open>(\<open>indent=1 notation=\<open>mixfix set interval\<close>\<close>{_<..<_})\<close>) where
"{l<..<u} == {l<..} Int {..<u}"
definition
- atLeastLessThan :: "'a => 'a => 'a set" (\<open>(1{_..<_})\<close>) where
+ atLeastLessThan :: "'a => 'a => 'a set" (\<open>(\<open>indent=1 notation=\<open>mixfix set interval\<close>\<close>{_..<_})\<close>) where
"{l..<u} == {l..} Int {..<u}"
definition
- greaterThanAtMost :: "'a => 'a => 'a set" (\<open>(1{_<.._})\<close>) where
+ greaterThanAtMost :: "'a => 'a => 'a set" (\<open>(\<open>indent=1 notation=\<open>mixfix set interval\<close>\<close>{_<.._})\<close>) where
"{l<..u} == {l<..} Int {..u}"
definition
- atLeastAtMost :: "'a => 'a => 'a set" (\<open>(1{_.._})\<close>) where
+ atLeastAtMost :: "'a => 'a => 'a set" (\<open>(\<open>indent=1 notation=\<open>mixfix set interval\<close>\<close>{_.._})\<close>) where
"{l..u} == {l..} Int {..u}"
end
@@ -67,10 +67,10 @@
\<^term>\<open>{m..<n}\<close> may not exist in \<^term>\<open>{..<n}\<close>-form as well.\<close>
syntax (ASCII)
- "_UNION_le" :: "'a => 'a => 'b set => 'b set" (\<open>(3UN _<=_./ _)\<close> [0, 0, 10] 10)
- "_UNION_less" :: "'a => 'a => 'b set => 'b set" (\<open>(3UN _<_./ _)\<close> [0, 0, 10] 10)
- "_INTER_le" :: "'a => 'a => 'b set => 'b set" (\<open>(3INT _<=_./ _)\<close> [0, 0, 10] 10)
- "_INTER_less" :: "'a => 'a => 'b set => 'b set" (\<open>(3INT _<_./ _)\<close> [0, 0, 10] 10)
+ "_UNION_le" :: "'a => 'a => 'b set => 'b set" (\<open>(\<open>indent=3 notation=\<open>binder UN\<close>\<close>UN _<=_./ _)\<close> [0, 0, 10] 10)
+ "_UNION_less" :: "'a => 'a => 'b set => 'b set" (\<open>(\<open>indent=3 notation=\<open>binder UN\<close>\<close>UN _<_./ _)\<close> [0, 0, 10] 10)
+ "_INTER_le" :: "'a => 'a => 'b set => 'b set" (\<open>(\<open>indent=3 notation=\<open>binder INT\<close>\<close>INT _<=_./ _)\<close> [0, 0, 10] 10)
+ "_INTER_less" :: "'a => 'a => 'b set => 'b set" (\<open>(\<open>indent=3 notation=\<open>binder INT\<close>\<close>INT _<_./ _)\<close> [0, 0, 10] 10)
syntax (latex output)
"_UNION_le" :: "'a \<Rightarrow> 'a => 'b set => 'b set" (\<open>(3\<Union>(\<open>unbreakable\<close>_ \<le> _)/ _)\<close> [0, 0, 10] 10)
@@ -79,10 +79,10 @@
"_INTER_less" :: "'a \<Rightarrow> 'a => 'b set => 'b set" (\<open>(3\<Inter>(\<open>unbreakable\<close>_ < _)/ _)\<close> [0, 0, 10] 10)
syntax
- "_UNION_le" :: "'a => 'a => 'b set => 'b set" (\<open>(3\<Union>_\<le>_./ _)\<close> [0, 0, 10] 10)
- "_UNION_less" :: "'a => 'a => 'b set => 'b set" (\<open>(3\<Union>_<_./ _)\<close> [0, 0, 10] 10)
- "_INTER_le" :: "'a => 'a => 'b set => 'b set" (\<open>(3\<Inter>_\<le>_./ _)\<close> [0, 0, 10] 10)
- "_INTER_less" :: "'a => 'a => 'b set => 'b set" (\<open>(3\<Inter>_<_./ _)\<close> [0, 0, 10] 10)
+ "_UNION_le" :: "'a => 'a => 'b set => 'b set" (\<open>(\<open>indent=3 notation=\<open>binder \<Union>\<close>\<close>\<Union>_\<le>_./ _)\<close> [0, 0, 10] 10)
+ "_UNION_less" :: "'a => 'a => 'b set => 'b set" (\<open>(\<open>indent=3 notation=\<open>binder \<Union>\<close>\<close>\<Union>_<_./ _)\<close> [0, 0, 10] 10)
+ "_INTER_le" :: "'a => 'a => 'b set => 'b set" (\<open>(\<open>indent=3 notation=\<open>binder \<Inter>\<close>\<close>\<Inter>_\<le>_./ _)\<close> [0, 0, 10] 10)
+ "_INTER_less" :: "'a => 'a => 'b set => 'b set" (\<open>(\<open>indent=3 notation=\<open>binder \<Inter>\<close>\<close>\<Inter>_<_./ _)\<close> [0, 0, 10] 10)
syntax_consts
"_UNION_le" "_UNION_less" \<rightleftharpoons> Union and
@@ -1988,10 +1988,10 @@
subsection \<open>Summation indexed over intervals\<close>
syntax (ASCII)
- "_from_to_sum" :: "idt \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b" (\<open>(SUM _ = _.._./ _)\<close> [0,0,0,10] 10)
- "_from_upto_sum" :: "idt \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b" (\<open>(SUM _ = _..<_./ _)\<close> [0,0,0,10] 10)
- "_upt_sum" :: "idt \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b" (\<open>(SUM _<_./ _)\<close> [0,0,10] 10)
- "_upto_sum" :: "idt \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b" (\<open>(SUM _<=_./ _)\<close> [0,0,10] 10)
+ "_from_to_sum" :: "idt \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b" (\<open>(\<open>notation=\<open>binder SUM\<close>\<close>SUM _ = _.._./ _)\<close> [0,0,0,10] 10)
+ "_from_upto_sum" :: "idt \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b" (\<open>(\<open>notation=\<open>binder SUM\<close>\<close>SUM _ = _..<_./ _)\<close> [0,0,0,10] 10)
+ "_upt_sum" :: "idt \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b" (\<open>(\<open>notation=\<open>binder SUM\<close>\<close>SUM _<_./ _)\<close> [0,0,10] 10)
+ "_upto_sum" :: "idt \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b" (\<open>(\<open>notation=\<open>binder SUM\<close>\<close>SUM _<=_./ _)\<close> [0,0,10] 10)
syntax (latex_sum output)
"_from_to_sum" :: "idt \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b"
@@ -2004,10 +2004,10 @@
(\<open>(3\<^latex>\<open>$\sum_{\<close>_ \<le> _\<^latex>\<open>}$\<close> _)\<close> [0,0,10] 10)
syntax
- "_from_to_sum" :: "idt \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b" (\<open>(3\<Sum>_ = _.._./ _)\<close> [0,0,0,10] 10)
- "_from_upto_sum" :: "idt \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b" (\<open>(3\<Sum>_ = _..<_./ _)\<close> [0,0,0,10] 10)
- "_upt_sum" :: "idt \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b" (\<open>(3\<Sum>_<_./ _)\<close> [0,0,10] 10)
- "_upto_sum" :: "idt \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b" (\<open>(3\<Sum>_\<le>_./ _)\<close> [0,0,10] 10)
+ "_from_to_sum" :: "idt \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b" (\<open>(\<open>indent=3 notation=\<open>binder \<Sum>\<close>\<close>\<Sum>_ = _.._./ _)\<close> [0,0,0,10] 10)
+ "_from_upto_sum" :: "idt \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b" (\<open>(\<open>indent=3 notation=\<open>binder \<Sum>\<close>\<close>\<Sum>_ = _..<_./ _)\<close> [0,0,0,10] 10)
+ "_upt_sum" :: "idt \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b" (\<open>(\<open>indent=3 notation=\<open>binder \<Sum>\<close>\<close>\<Sum>_<_./ _)\<close> [0,0,10] 10)
+ "_upto_sum" :: "idt \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b" (\<open>(\<open>indent=3 notation=\<open>binder \<Sum>\<close>\<close>\<Sum>_\<le>_./ _)\<close> [0,0,10] 10)
syntax_consts
"_from_to_sum" "_from_upto_sum" "_upt_sum" "_upto_sum" == sum
@@ -2681,10 +2681,10 @@
subsection \<open>Products indexed over intervals\<close>
syntax (ASCII)
- "_from_to_prod" :: "idt \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b" (\<open>(PROD _ = _.._./ _)\<close> [0,0,0,10] 10)
- "_from_upto_prod" :: "idt \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b" (\<open>(PROD _ = _..<_./ _)\<close> [0,0,0,10] 10)
- "_upt_prod" :: "idt \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b" (\<open>(PROD _<_./ _)\<close> [0,0,10] 10)
- "_upto_prod" :: "idt \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b" (\<open>(PROD _<=_./ _)\<close> [0,0,10] 10)
+ "_from_to_prod" :: "idt \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b" (\<open>(\<open>notation=\<open>binder PROD\<close>\<close>PROD _ = _.._./ _)\<close> [0,0,0,10] 10)
+ "_from_upto_prod" :: "idt \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b" (\<open>(\<open>notation=\<open>binder PROD\<close>\<close>PROD _ = _..<_./ _)\<close> [0,0,0,10] 10)
+ "_upt_prod" :: "idt \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b" (\<open>(\<open>notation=\<open>binder PROD\<close>\<close>PROD _<_./ _)\<close> [0,0,10] 10)
+ "_upto_prod" :: "idt \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b" (\<open>(\<open>notation=\<open>binder PROD\<close>\<close>PROD _<=_./ _)\<close> [0,0,10] 10)
syntax (latex_prod output)
"_from_to_prod" :: "idt \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b"
@@ -2697,10 +2697,10 @@
(\<open>(3\<^latex>\<open>$\prod_{\<close>_ \<le> _\<^latex>\<open>}$\<close> _)\<close> [0,0,10] 10)
syntax
- "_from_to_prod" :: "idt \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b" (\<open>(3\<Prod>_ = _.._./ _)\<close> [0,0,0,10] 10)
- "_from_upto_prod" :: "idt \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b" (\<open>(3\<Prod>_ = _..<_./ _)\<close> [0,0,0,10] 10)
- "_upt_prod" :: "idt \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b" (\<open>(3\<Prod>_<_./ _)\<close> [0,0,10] 10)
- "_upto_prod" :: "idt \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b" (\<open>(3\<Prod>_\<le>_./ _)\<close> [0,0,10] 10)
+ "_from_to_prod" :: "idt \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b" (\<open>(\<open>indent=3 notation=\<open>binder \<Prod>\<close>\<close>\<Prod>_ = _.._./ _)\<close> [0,0,0,10] 10)
+ "_from_upto_prod" :: "idt \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b" (\<open>(\<open>indent=3 notation=\<open>binder \<Prod>\<close>\<close>\<Prod>_ = _..<_./ _)\<close> [0,0,0,10] 10)
+ "_upt_prod" :: "idt \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b" (\<open>(\<open>indent=3 notation=\<open>binder \<Prod>\<close>\<close>\<Prod>_<_./ _)\<close> [0,0,10] 10)
+ "_upto_prod" :: "idt \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b" (\<open>(\<open>indent=3 notation=\<open>binder \<Prod>\<close>\<close>\<Prod>_\<le>_./ _)\<close> [0,0,10] 10)
syntax_consts
"_from_to_prod" "_from_upto_prod" "_upt_prod" "_upto_prod" \<rightleftharpoons> prod
--- a/src/HOL/Topological_Spaces.thy Mon Sep 23 15:01:10 2024 +0200
+++ b/src/HOL/Topological_Spaces.thy Mon Sep 23 21:09:23 2024 +0200
@@ -1191,7 +1191,7 @@
subsection \<open>Limits on sequences\<close>
abbreviation (in topological_space)
- LIMSEQ :: "[nat \<Rightarrow> 'a, 'a] \<Rightarrow> bool" (\<open>((_)/ \<longlonglongrightarrow> (_))\<close> [60, 60] 60)
+ LIMSEQ :: "[nat \<Rightarrow> 'a, 'a] \<Rightarrow> bool" (\<open>(\<open>notation=\<open>infix LIMSEQ\<close>\<close>(_)/ \<longlonglongrightarrow> (_))\<close> [60, 60] 60)
where "X \<longlonglongrightarrow> L \<equiv> (X \<longlongrightarrow> L) sequentially"
abbreviation (in t2_space) lim :: "(nat \<Rightarrow> 'a) \<Rightarrow> 'a"
@@ -1760,7 +1760,7 @@
subsection \<open>Function limit at a point\<close>
abbreviation LIM :: "('a::topological_space \<Rightarrow> 'b::topological_space) \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> bool"
- (\<open>((_)/ \<midarrow>(_)/\<rightarrow> (_))\<close> [60, 0, 60] 60)
+ (\<open>(\<open>notation=\<open>infix LIM\<close>\<close>(_)/ \<midarrow>(_)/\<rightarrow> (_))\<close> [60, 0, 60] 60)
where "f \<midarrow>a\<rightarrow> L \<equiv> (f \<longlongrightarrow> L) (at a)"
lemma tendsto_within_open: "a \<in> S \<Longrightarrow> open S \<Longrightarrow> (f \<longlongrightarrow> l) (at a within S) \<longleftrightarrow> (f \<midarrow>a\<rightarrow> l)"
--- a/src/HOL/Transitive_Closure.thy Mon Sep 23 15:01:10 2024 +0200
+++ b/src/HOL/Transitive_Closure.thy Mon Sep 23 21:09:23 2024 +0200
@@ -26,21 +26,21 @@
context notes [[inductive_internals]]
begin
-inductive_set rtrancl :: "('a \<times> 'a) set \<Rightarrow> ('a \<times> 'a) set" (\<open>(_\<^sup>*)\<close> [1000] 999)
+inductive_set rtrancl :: "('a \<times> 'a) set \<Rightarrow> ('a \<times> 'a) set" (\<open>(\<open>notation=\<open>postfix *\<close>\<close>_\<^sup>*)\<close> [1000] 999)
for r :: "('a \<times> 'a) set"
where
rtrancl_refl [intro!, Pure.intro!, simp]: "(a, a) \<in> r\<^sup>*"
| rtrancl_into_rtrancl [Pure.intro]: "(a, b) \<in> r\<^sup>* \<Longrightarrow> (b, c) \<in> r \<Longrightarrow> (a, c) \<in> r\<^sup>*"
-inductive_set trancl :: "('a \<times> 'a) set \<Rightarrow> ('a \<times> 'a) set" (\<open>(_\<^sup>+)\<close> [1000] 999)
+inductive_set trancl :: "('a \<times> 'a) set \<Rightarrow> ('a \<times> 'a) set" (\<open>(\<open>notation=\<open>postfix +\<close>\<close>_\<^sup>+)\<close> [1000] 999)
for r :: "('a \<times> 'a) set"
where
r_into_trancl [intro, Pure.intro]: "(a, b) \<in> r \<Longrightarrow> (a, b) \<in> r\<^sup>+"
| trancl_into_trancl [Pure.intro]: "(a, b) \<in> r\<^sup>+ \<Longrightarrow> (b, c) \<in> r \<Longrightarrow> (a, c) \<in> r\<^sup>+"
notation
- rtranclp (\<open>(_\<^sup>*\<^sup>*)\<close> [1000] 1000) and
- tranclp (\<open>(_\<^sup>+\<^sup>+)\<close> [1000] 1000)
+ rtranclp (\<open>(\<open>notation=\<open>postfix **\<close>\<close>_\<^sup>*\<^sup>*)\<close> [1000] 1000) and
+ tranclp (\<open>(\<open>notation=\<open>postfix ++\<close>\<close>_\<^sup>+\<^sup>+)\<close> [1000] 1000)
declare
rtrancl_def [nitpick_unfold del]
@@ -50,19 +50,19 @@
end
-abbreviation reflcl :: "('a \<times> 'a) set \<Rightarrow> ('a \<times> 'a) set" (\<open>(_\<^sup>=)\<close> [1000] 999)
+abbreviation reflcl :: "('a \<times> 'a) set \<Rightarrow> ('a \<times> 'a) set" (\<open>(\<open>notation=\<open>postfix =\<close>\<close>_\<^sup>=)\<close> [1000] 999)
where "r\<^sup>= \<equiv> r \<union> Id"
-abbreviation reflclp :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> bool" (\<open>(_\<^sup>=\<^sup>=)\<close> [1000] 1000)
+abbreviation reflclp :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> bool" (\<open>(\<open>notation=\<open>postfix ==\<close>\<close>_\<^sup>=\<^sup>=)\<close> [1000] 1000)
where "r\<^sup>=\<^sup>= \<equiv> sup r (=)"
notation (ASCII)
- rtrancl (\<open>(_^*)\<close> [1000] 999) and
- trancl (\<open>(_^+)\<close> [1000] 999) and
- reflcl (\<open>(_^=)\<close> [1000] 999) and
- rtranclp (\<open>(_^**)\<close> [1000] 1000) and
- tranclp (\<open>(_^++)\<close> [1000] 1000) and
- reflclp (\<open>(_^==)\<close> [1000] 1000)
+ rtrancl (\<open>(\<open>notation=\<open>postfix *\<close>\<close>_^*)\<close> [1000] 999) and
+ trancl (\<open>(\<open>notation=\<open>postfix +\<close>\<close>_^+)\<close> [1000] 999) and
+ reflcl (\<open>(\<open>notation=\<open>postfix =\<close>\<close>_^=)\<close> [1000] 999) and
+ rtranclp (\<open>(\<open>notation=\<open>postfix **\<close>\<close>_^**)\<close> [1000] 1000) and
+ tranclp (\<open>(\<open>notation=\<open>postfix ++\<close>\<close>_^++)\<close> [1000] 1000) and
+ reflclp (\<open>(\<open>notation=\<open>postfix ==\<close>\<close>_^==)\<close> [1000] 1000)
subsection \<open>Reflexive closure\<close>
--- a/src/HOL/Typerep.thy Mon Sep 23 15:01:10 2024 +0200
+++ b/src/HOL/Typerep.thy Mon Sep 23 21:09:23 2024 +0200
@@ -18,7 +18,7 @@
end
syntax
- "_TYPEREP" :: "type => logic" (\<open>(1TYPEREP/(1'(_')))\<close>)
+ "_TYPEREP" :: "type => logic" (\<open>(\<open>indent=1 notation=\<open>prefix TYPEREP\<close>\<close>TYPEREP/(1'(_')))\<close>)
syntax_consts
"_TYPEREP" \<rightleftharpoons> typerep