--- a/src/HOL/Algebra/AbelCoset.thy Wed Oct 09 22:01:33 2024 +0200
+++ b/src/HOL/Algebra/AbelCoset.thy Wed Oct 09 23:38:29 2024 +0200
@@ -24,7 +24,8 @@
where "a_l_coset G = l_coset (add_monoid G)"
definition
- A_RCOSETS :: "[_, 'a set] \<Rightarrow> ('a set)set" (\<open>a'_rcosets\<index> _\<close> [81] 80)
+ A_RCOSETS :: "[_, 'a set] \<Rightarrow> ('a set)set"
+ (\<open>(\<open>open_block notation=\<open>prefix a_rcosets\<close>\<close>a'_rcosets\<index> _)\<close> [81] 80)
where "A_RCOSETS G H = RCOSETS (add_monoid G) H"
definition
@@ -32,7 +33,8 @@
where "set_add G = set_mult (add_monoid G)"
definition
- A_SET_INV :: "[_,'a set] \<Rightarrow> 'a set" (\<open>a'_set'_inv\<index> _\<close> [81] 80)
+ A_SET_INV :: "[_,'a set] \<Rightarrow> 'a set"
+ (\<open>(\<open>open_block notation=\<open>prefix a_set_inv\<close>\<close>a'_set'_inv\<index> _)\<close> [81] 80)
where "A_SET_INV G H = SET_INV (add_monoid G) H"
definition
--- a/src/HOL/Algebra/Algebraic_Closure_Type.thy Wed Oct 09 22:01:33 2024 +0200
+++ b/src/HOL/Algebra/Algebraic_Closure_Type.thy Wed Oct 09 23:38:29 2024 +0200
@@ -468,8 +468,8 @@
bundle alg_closure_syntax
begin
-notation to_ac (\<open>_\<up>\<close> [1000] 999)
-notation of_ac (\<open>_\<down>\<close> [1000] 999)
+notation to_ac (\<open>(\<open>open_block notation=\<open>postfix \<up>\<close>\<close>_\<up>)\<close> [1000] 999)
+notation of_ac (\<open>(\<open>open_block notation=\<open>postfix \<down>\<close>\<close>_\<down>)\<close> [1000] 999)
end
--- a/src/HOL/Algebra/Coset.thy Wed Oct 09 22:01:33 2024 +0200
+++ b/src/HOL/Algebra/Coset.thy Wed Oct 09 23:38:29 2024 +0200
@@ -19,7 +19,8 @@
where "a <#\<^bsub>G\<^esub> H = (\<Union>h\<in>H. {a \<otimes>\<^bsub>G\<^esub> h})"
definition
- RCOSETS :: "[_, 'a set] \<Rightarrow> ('a set)set" (\<open>rcosets\<index> _\<close> [81] 80)
+ RCOSETS :: "[_, 'a set] \<Rightarrow> ('a set)set"
+ (\<open>(\<open>open_block notation=\<open>prefix rcosets\<close>\<close>rcosets\<index> _)\<close> [81] 80)
where "rcosets\<^bsub>G\<^esub> H = (\<Union>a\<in>carrier G. {H #>\<^bsub>G\<^esub> a})"
definition
@@ -27,7 +28,8 @@
where "H <#>\<^bsub>G\<^esub> K = (\<Union>h\<in>H. \<Union>k\<in>K. {h \<otimes>\<^bsub>G\<^esub> k})"
definition
- SET_INV :: "[_,'a set] \<Rightarrow> 'a set" (\<open>set'_inv\<index> _\<close> [81] 80)
+ SET_INV :: "[_,'a set] \<Rightarrow> 'a set"
+ (\<open>(\<open>open_block notation=\<open>prefix set_inv\<close>\<close>set'_inv\<index> _)\<close> [81] 80)
where "set_inv\<^bsub>G\<^esub> H = (\<Union>h\<in>H. {inv\<^bsub>G\<^esub> h})"
@@ -659,7 +661,8 @@
subsubsection\<open>An Equivalence Relation\<close>
definition
- r_congruent :: "[('a,'b)monoid_scheme, 'a set] \<Rightarrow> ('a*'a)set" (\<open>rcong\<index> _\<close>)
+ r_congruent :: "[('a,'b)monoid_scheme, 'a set] \<Rightarrow> ('a*'a)set"
+ (\<open>(\<open>open_block notation=\<open>prefix rcong\<close>\<close>rcong\<index> _)\<close>)
where "rcong\<^bsub>G\<^esub> H = {(x,y). x \<in> carrier G \<and> y \<in> carrier G \<and> inv\<^bsub>G\<^esub> x \<otimes>\<^bsub>G\<^esub> y \<in> H}"
--- a/src/HOL/Algebra/Divisibility.thy Wed Oct 09 22:01:33 2024 +0200
+++ b/src/HOL/Algebra/Divisibility.thy Wed Oct 09 23:38:29 2024 +0200
@@ -1993,11 +1993,13 @@
subsubsection \<open>Definitions\<close>
-definition isgcd :: "[('a,_) monoid_scheme, 'a, 'a, 'a] \<Rightarrow> bool" (\<open>(_ gcdof\<index> _ _)\<close> [81,81,81] 80)
+definition isgcd :: "[('a,_) monoid_scheme, 'a, 'a, 'a] \<Rightarrow> bool"
+ (\<open>(\<open>notation=\<open>mixfix gcdof\<close>\<close>_ gcdof\<index> _ _)\<close> [81,81,81] 80)
where "x gcdof\<^bsub>G\<^esub> a b \<longleftrightarrow> x divides\<^bsub>G\<^esub> a \<and> x divides\<^bsub>G\<^esub> b \<and>
(\<forall>y\<in>carrier G. (y divides\<^bsub>G\<^esub> a \<and> y divides\<^bsub>G\<^esub> b \<longrightarrow> y divides\<^bsub>G\<^esub> x))"
-definition islcm :: "[_, 'a, 'a, 'a] \<Rightarrow> bool" (\<open>(_ lcmof\<index> _ _)\<close> [81,81,81] 80)
+definition islcm :: "[_, 'a, 'a, 'a] \<Rightarrow> bool"
+ (\<open>(\<open>notation=\<open>mixfix lcmof\<close>\<close>_ lcmof\<index> _ _)\<close> [81,81,81] 80)
where "x lcmof\<^bsub>G\<^esub> a b \<longleftrightarrow> a divides\<^bsub>G\<^esub> x \<and> b divides\<^bsub>G\<^esub> x \<and>
(\<forall>y\<in>carrier G. (a divides\<^bsub>G\<^esub> y \<and> b divides\<^bsub>G\<^esub> y \<longrightarrow> x divides\<^bsub>G\<^esub> y))"
--- a/src/HOL/Algebra/Exact_Sequence.thy Wed Oct 09 22:01:33 2024 +0200
+++ b/src/HOL/Algebra/Exact_Sequence.thy Wed Oct 09 23:38:29 2024 +0200
@@ -22,7 +22,7 @@
abbreviation exact_seq_arrow ::
"('a \<Rightarrow> 'a) \<Rightarrow> 'a monoid list \<times> ('a \<Rightarrow> 'a) list \<Rightarrow> 'a monoid \<Rightarrow> 'a monoid list \<times> ('a \<Rightarrow> 'a) list"
- (\<open>(3_ / \<longlongrightarrow>\<index> _)\<close> [1000, 60])
+ (\<open>(\<open>indent=3 notation=\<open>mixfix exact_seq\<close>\<close>_ / \<longlongrightarrow>\<index> _)\<close> [1000, 60])
where "exact_seq_arrow f t G \<equiv> (G # (fst t), f # (snd t))"
--- a/src/HOL/Algebra/FiniteProduct.thy Wed Oct 09 22:01:33 2024 +0200
+++ b/src/HOL/Algebra/FiniteProduct.thy Wed Oct 09 23:38:29 2024 +0200
@@ -307,7 +307,7 @@
syntax
"_finprod" :: "index \<Rightarrow> idt \<Rightarrow> 'a set \<Rightarrow> 'b \<Rightarrow> 'b"
- (\<open>(3\<Otimes>__\<in>_. _)\<close> [1000, 0, 51, 10] 10)
+ (\<open>(\<open>indent=3 notation=\<open>binder \<Otimes>\<close>\<close>\<Otimes>__\<in>_. _)\<close> [1000, 0, 51, 10] 10)
syntax_consts
"_finprod" \<rightleftharpoons> finprod
translations
--- a/src/HOL/Algebra/Group.thy Wed Oct 09 22:01:33 2024 +0200
+++ b/src/HOL/Algebra/Group.thy Wed Oct 09 23:38:29 2024 +0200
@@ -22,7 +22,8 @@
one :: 'a (\<open>\<one>\<index>\<close>)
definition
- m_inv :: "('a, 'b) monoid_scheme => 'a => 'a" (\<open>inv\<index> _\<close> [81] 80)
+ m_inv :: "('a, 'b) monoid_scheme => 'a => 'a"
+ (\<open>(\<open>open_block notation=\<open>prefix inv\<close>\<close>inv\<index> _)\<close> [81] 80)
where "inv\<^bsub>G\<^esub> x = (THE y. y \<in> carrier G \<and> x \<otimes>\<^bsub>G\<^esub> y = \<one>\<^bsub>G\<^esub> \<and> y \<otimes>\<^bsub>G\<^esub> x = \<one>\<^bsub>G\<^esub>)"
definition
--- a/src/HOL/Algebra/Ideal.thy Wed Oct 09 22:01:33 2024 +0200
+++ b/src/HOL/Algebra/Ideal.thy Wed Oct 09 23:38:29 2024 +0200
@@ -45,8 +45,9 @@
subsubsection (in ring) \<open>Ideals Generated by a Subset of \<^term>\<open>carrier R\<close>\<close>
-definition genideal :: "_ \<Rightarrow> 'a set \<Rightarrow> 'a set" (\<open>Idl\<index> _\<close> [80] 79)
- where "genideal R S = \<Inter>{I. ideal I R \<and> S \<subseteq> I}"
+definition genideal :: "_ \<Rightarrow> 'a set \<Rightarrow> 'a set"
+ (\<open>(\<open>open_block notation=\<open>prefix Idl\<close>\<close>Idl\<index> _)\<close> [80] 79)
+ where "Idl\<^bsub>R\<^esub> S = \<Inter>{I. ideal I R \<and> S \<subseteq> I}"
subsubsection \<open>Principal Ideals\<close>
@@ -411,8 +412,9 @@
text \<open>Generation of Principal Ideals in Commutative Rings\<close>
-definition cgenideal :: "_ \<Rightarrow> 'a \<Rightarrow> 'a set" (\<open>PIdl\<index> _\<close> [80] 79)
- where "cgenideal R a = {x \<otimes>\<^bsub>R\<^esub> a | x. x \<in> carrier R}"
+definition cgenideal :: "_ \<Rightarrow> 'a \<Rightarrow> 'a set"
+ (\<open>(\<open>open_block notation=\<open>prefix PIdl\<close>\<close>PIdl\<index> _)\<close> [80] 79)
+ where "PIdl\<^bsub>R\<^esub> a = {x \<otimes>\<^bsub>R\<^esub> a | x. x \<in> carrier R}"
text \<open>genhideal (?) really generates an ideal\<close>
lemma (in cring) cgenideal_ideal:
--- a/src/HOL/Algebra/Indexed_Polynomials.thy Wed Oct 09 22:01:33 2024 +0200
+++ b/src/HOL/Algebra/Indexed_Polynomials.thy Wed Oct 09 23:38:29 2024 +0200
@@ -38,7 +38,8 @@
definition (in ring) carrier_coeff :: "('c multiset \<Rightarrow> 'a) \<Rightarrow> bool"
where "carrier_coeff P \<longleftrightarrow> (\<forall>m. P m \<in> carrier R)"
-inductive_set (in ring) indexed_pset :: "'c set \<Rightarrow> 'a set \<Rightarrow> ('c multiset \<Rightarrow> 'a) set" (\<open>_ [\<X>\<index>]\<close> 80)
+inductive_set (in ring) indexed_pset :: "'c set \<Rightarrow> 'a set \<Rightarrow> ('c multiset \<Rightarrow> 'a) set"
+ (\<open>(\<open>open_block notation=\<open>postfix \<X>\<close>\<close>_ [\<X>\<index>])\<close> 80)
for I and K where
indexed_const: "k \<in> K \<Longrightarrow> indexed_const k \<in> (K[\<X>\<^bsub>I\<^esub>])"
| indexed_padd: "\<lbrakk> P \<in> (K[\<X>\<^bsub>I\<^esub>]); Q \<in> (K[\<X>\<^bsub>I\<^esub>]) \<rbrakk> \<Longrightarrow> P \<Oplus> Q \<in> (K[\<X>\<^bsub>I\<^esub>])"
--- a/src/HOL/Algebra/Lattice.thy Wed Oct 09 22:01:33 2024 +0200
+++ b/src/HOL/Algebra/Lattice.thy Wed Oct 09 23:38:29 2024 +0200
@@ -15,11 +15,11 @@
subsection \<open>Supremum and infimum\<close>
definition
- sup :: "[_, 'a set] => 'a" (\<open>\<Squnion>\<index>_\<close> [90] 90)
+ sup :: "[_, 'a set] => 'a" (\<open>(\<open>open_block notation=\<open>prefix \<Squnion>\<close>\<close>\<Squnion>\<index>_)\<close> [90] 90)
where "\<Squnion>\<^bsub>L\<^esub>A = (SOME x. least L x (Upper L A))"
definition
- inf :: "[_, 'a set] => 'a" (\<open>\<Sqinter>\<index>_\<close> [90] 90)
+ inf :: "[_, 'a set] => 'a" (\<open>(\<open>open_block notation=\<open>prefix \<Sqinter>\<close>\<close>\<Sqinter>\<index>_)\<close> [90] 90)
where "\<Sqinter>\<^bsub>L\<^esub>A = (SOME x. greatest L x (Lower L A))"
definition supr ::
@@ -31,15 +31,17 @@
where "infi L A f = \<Sqinter>\<^bsub>L\<^esub>(f ` A)"
syntax
- "_inf1" :: "('a, 'b) gorder_scheme \<Rightarrow> pttrns \<Rightarrow> 'a \<Rightarrow> 'a" (\<open>(3IINF\<index> _./ _)\<close> [0, 10] 10)
- "_inf" :: "('a, 'b) gorder_scheme \<Rightarrow> pttrn \<Rightarrow> 'c set \<Rightarrow> 'a \<Rightarrow> 'a" (\<open>(3IINF\<index> _:_./ _)\<close> [0, 0, 10] 10)
- "_sup1" :: "('a, 'b) gorder_scheme \<Rightarrow> pttrns \<Rightarrow> 'a \<Rightarrow> 'a" (\<open>(3SSUP\<index> _./ _)\<close> [0, 10] 10)
- "_sup" :: "('a, 'b) gorder_scheme \<Rightarrow> pttrn \<Rightarrow> 'c set \<Rightarrow> 'a \<Rightarrow> 'a" (\<open>(3SSUP\<index> _:_./ _)\<close> [0, 0, 10] 10)
-
+ "_inf1" :: "('a, 'b) gorder_scheme \<Rightarrow> pttrns \<Rightarrow> 'a \<Rightarrow> 'a"
+ (\<open>(\<open>indent=3 notation=\<open>binder IINF\<close>\<close>IINF\<index> _./ _)\<close> [0, 10] 10)
+ "_inf" :: "('a, 'b) gorder_scheme \<Rightarrow> pttrn \<Rightarrow> 'c set \<Rightarrow> 'a \<Rightarrow> 'a"
+ (\<open>(\<open>indent=3 notation=\<open>binder IINF\<close>\<close>IINF\<index> _:_./ _)\<close> [0, 0, 10] 10)
+ "_sup1" :: "('a, 'b) gorder_scheme \<Rightarrow> pttrns \<Rightarrow> 'a \<Rightarrow> 'a"
+ (\<open>(\<open>indent=3 notation=\<open>binder SSUP\<close>\<close>SSUP\<index> _./ _)\<close> [0, 10] 10)
+ "_sup" :: "('a, 'b) gorder_scheme \<Rightarrow> pttrn \<Rightarrow> 'c set \<Rightarrow> 'a \<Rightarrow> 'a"
+ (\<open>(\<open>indent=3 notation=\<open>binder SSUP\<close>\<close>SSUP\<index> _:_./ _)\<close> [0, 0, 10] 10)
syntax_consts
"_inf1" "_inf" == infi and
"_sup1" "_sup" == supr
-
translations
"IINF\<^bsub>L\<^esub> x. B" == "CONST infi L CONST UNIV (%x. B)"
"IINF\<^bsub>L\<^esub> x:A. B" == "CONST infi L A (%x. B)"
--- a/src/HOL/Algebra/Left_Coset.thy Wed Oct 09 22:01:33 2024 +0200
+++ b/src/HOL/Algebra/Left_Coset.thy Wed Oct 09 23:38:29 2024 +0200
@@ -7,7 +7,8 @@
begin
definition
- LCOSETS :: "[_, 'a set] \<Rightarrow> ('a set)set" (\<open>lcosets\<index> _\<close> [81] 80)
+ LCOSETS :: "[_, 'a set] \<Rightarrow> ('a set)set"
+ (\<open>(\<open>open_block notation=\<open>prefix lcosets\<close>\<close>lcosets\<index> _)\<close> [81] 80)
where "lcosets\<^bsub>G\<^esub> H = (\<Union>a\<in>carrier G. {a <#\<^bsub>G\<^esub> H})"
definition
--- a/src/HOL/Algebra/Order.thy Wed Oct 09 22:01:33 2024 +0200
+++ b/src/HOL/Algebra/Order.thy Wed Oct 09 23:38:29 2024 +0200
@@ -411,7 +411,8 @@
subsubsection \<open>Intervals\<close>
definition
- at_least_at_most :: "('a, 'c) gorder_scheme \<Rightarrow> 'a => 'a => 'a set" (\<open>(1\<lbrace>_.._\<rbrace>\<index>)\<close>)
+ at_least_at_most :: "('a, 'c) gorder_scheme \<Rightarrow> 'a => 'a => 'a set"
+ (\<open>(\<open>indent=1 notation=\<open>mixfix interval\<close>\<close>\<lbrace>_.._\<rbrace>\<index>)\<close>)
where "\<lbrace>l..u\<rbrace>\<^bsub>A\<^esub> = {x \<in> carrier A. l \<sqsubseteq>\<^bsub>A\<^esub> x \<and> x \<sqsubseteq>\<^bsub>A\<^esub> u}"
context weak_partial_order
@@ -452,8 +453,9 @@
shows "isotone L1 L2 f"
using assms by (auto simp add:isotone_def)
-abbreviation Monotone :: "('a, 'b) gorder_scheme \<Rightarrow> ('a \<Rightarrow> 'a) \<Rightarrow> bool" (\<open>Mono\<index>\<close>)
- where "Monotone L f \<equiv> isotone L L f"
+abbreviation Monotone :: "('a, 'b) gorder_scheme \<Rightarrow> ('a \<Rightarrow> 'a) \<Rightarrow> bool"
+ (\<open>(\<open>open_block notation=\<open>prefix Mono\<close>\<close>Mono\<index>)\<close>)
+ where "Mono\<^bsub>L\<^esub> f \<equiv> isotone L L f"
lemma use_iso1:
"\<lbrakk>isotone A A f; x \<in> carrier A; y \<in> carrier A; x \<sqsubseteq>\<^bsub>A\<^esub> y\<rbrakk> \<Longrightarrow>
@@ -478,8 +480,9 @@
subsubsection \<open>Idempotent functions\<close>
definition idempotent ::
- "('a, 'b) gorder_scheme \<Rightarrow> ('a \<Rightarrow> 'a) \<Rightarrow> bool" (\<open>Idem\<index>\<close>) where
- "idempotent L f \<equiv> \<forall>x\<in>carrier L. f (f x) .=\<^bsub>L\<^esub> f x"
+ "('a, 'b) gorder_scheme \<Rightarrow> ('a \<Rightarrow> 'a) \<Rightarrow> bool"
+ (\<open>(\<open>open_block notation=\<open>prefix Idem\<close>\<close>Idem\<index>)\<close>)
+ where "Idem\<^bsub>L\<^esub> f \<equiv> \<forall>x\<in>carrier L. f (f x) .=\<^bsub>L\<^esub> f x"
lemma (in weak_partial_order) idempotent:
"\<lbrakk>Idem f; x \<in> carrier L\<rbrakk> \<Longrightarrow> f (f x) .= f x"
--- a/src/HOL/Algebra/Polynomials.thy Wed Oct 09 22:01:33 2024 +0200
+++ b/src/HOL/Algebra/Polynomials.thy Wed Oct 09 23:38:29 2024 +0200
@@ -1359,7 +1359,8 @@
subsection \<open>Algebraic Structure of Polynomials\<close>
-definition univ_poly :: "('a, 'b) ring_scheme \<Rightarrow>'a set \<Rightarrow> ('a list) ring" (\<open>_ [X]\<index>\<close> 80)
+definition univ_poly :: "('a, 'b) ring_scheme \<Rightarrow>'a set \<Rightarrow> ('a list) ring"
+ (\<open>(\<open>open_block notation=\<open>postfix X\<close>\<close>_ [X]\<index>)\<close> 80)
where "univ_poly R K =
\<lparr> carrier = { p. polynomial\<^bsub>R\<^esub> K p },
mult = ring.poly_mult R,
--- a/src/HOL/Algebra/QuotRing.thy Wed Oct 09 22:01:33 2024 +0200
+++ b/src/HOL/Algebra/QuotRing.thy Wed Oct 09 23:38:29 2024 +0200
@@ -12,7 +12,7 @@
subsection \<open>Multiplication on Cosets\<close>
definition rcoset_mult :: "[('a, _) ring_scheme, 'a set, 'a set, 'a set] \<Rightarrow> 'a set"
- (\<open>[mod _:] _ \<Otimes>\<index> _\<close> [81,81,81] 80)
+ (\<open>(\<open>open_block notation=\<open>mixfix rcoset_mult\<close>\<close>[mod _:] _ \<Otimes>\<index> _)\<close> [81,81,81] 80)
where "rcoset_mult R I A B = (\<Union>a\<in>A. \<Union>b\<in>B. I +>\<^bsub>R\<^esub> (a \<otimes>\<^bsub>R\<^esub> b))"
--- a/src/HOL/Algebra/Ring.thy Wed Oct 09 22:01:33 2024 +0200
+++ b/src/HOL/Algebra/Ring.thy Wed Oct 09 23:38:29 2024 +0200
@@ -23,16 +23,17 @@
text \<open>Derived operations.\<close>
definition
- a_inv :: "[('a, 'm) ring_scheme, 'a ] \<Rightarrow> 'a" (\<open>\<ominus>\<index> _\<close> [81] 80)
+ a_inv :: "[('a, 'm) ring_scheme, 'a ] \<Rightarrow> 'a" (\<open>(\<open>open_block notation=\<open>prefix \<ominus>\<close>\<close>\<ominus>\<index> _)\<close> [81] 80)
where "a_inv R = m_inv (add_monoid R)"
definition
- a_minus :: "[('a, 'm) ring_scheme, 'a, 'a] => 'a" (\<open>(_ \<ominus>\<index> _)\<close> [65,66] 65)
+ a_minus :: "[('a, 'm) ring_scheme, 'a, 'a] => 'a" (\<open>(\<open>notation=\<open>infix \<ominus>\<close>\<close>_ \<ominus>\<index> _)\<close> [65,66] 65)
where "x \<ominus>\<^bsub>R\<^esub> y = x \<oplus>\<^bsub>R\<^esub> (\<ominus>\<^bsub>R\<^esub> y)"
definition
- add_pow :: "[_, ('b :: semiring_1), 'a] \<Rightarrow> 'a" (\<open>[_] \<cdot>\<index> _\<close> [81, 81] 80)
- where "add_pow R k a = pow (add_monoid R) a k"
+ add_pow :: "[_, ('b :: semiring_1), 'a] \<Rightarrow> 'a"
+ (\<open>(\<open>open_block notation=\<open>mixfix \<cdot>\<close>\<close>[_] \<cdot>\<index> _)\<close> [81, 81] 80)
+ where "[k] \<cdot>\<^bsub>R\<^esub> a = pow (add_monoid R) a k"
locale abelian_monoid =
fixes G (structure)
@@ -45,7 +46,7 @@
syntax
"_finsum" :: "index \<Rightarrow> idt \<Rightarrow> 'a set \<Rightarrow> 'b \<Rightarrow> 'b"
- (\<open>(3\<Oplus>__\<in>_. _)\<close> [1000, 0, 51, 10] 10)
+ (\<open>(\<open>indent=3 notation=\<open>binder \<Oplus>\<close>\<close>\<Oplus>__\<in>_. _)\<close> [1000, 0, 51, 10] 10)
syntax_consts
"_finsum" \<rightleftharpoons> finsum
translations
--- a/src/HOL/Analysis/Euclidean_Space.thy Wed Oct 09 22:01:33 2024 +0200
+++ b/src/HOL/Analysis/Euclidean_Space.thy Wed Oct 09 23:38:29 2024 +0200
@@ -33,7 +33,7 @@
assumes euclidean_all_zero_iff:
"(\<forall>u\<in>Basis. inner x u = 0) \<longleftrightarrow> (x = 0)"
-syntax "_type_dimension" :: "type \<Rightarrow> nat" (\<open>(1DIM/(1'(_')))\<close>)
+syntax "_type_dimension" :: "type \<Rightarrow> nat" (\<open>(\<open>indent=1 notation=\<open>mixfix type dimension\<close>\<close>DIM/(1'(_')))\<close>)
syntax_consts "_type_dimension" \<rightleftharpoons> card
translations "DIM('a)" \<rightharpoonup> "CONST card (CONST Basis :: 'a set)"
typed_print_translation \<open>
--- a/src/HOL/Analysis/Lipschitz.thy Wed Oct 09 22:01:33 2024 +0200
+++ b/src/HOL/Analysis/Lipschitz.thy Wed Oct 09 23:38:29 2024 +0200
@@ -14,7 +14,8 @@
open_bundle lipschitz_syntax
begin
-notation\<^marker>\<open>tag important\<close> lipschitz_on (\<open>_-lipschitz'_on\<close> [1000])
+notation\<^marker>\<open>tag important\<close>
+ lipschitz_on (\<open>(\<open>open_block notation=\<open>postfix lipschitz_on\<close>\<close>_-lipschitz'_on)\<close> [1000])
end
lemma lipschitz_onI: "L-lipschitz_on X f"
--- a/src/HOL/Analysis/Measure_Space.thy Wed Oct 09 22:01:33 2024 +0200
+++ b/src/HOL/Analysis/Measure_Space.thy Wed Oct 09 23:38:29 2024 +0200
@@ -1004,11 +1004,10 @@
"almost_everywhere M P \<equiv> eventually P (ae_filter M)"
syntax
- "_almost_everywhere" :: "pttrn \<Rightarrow> 'a \<Rightarrow> bool \<Rightarrow> bool" (\<open>AE _ in _. _\<close> [0,0,10] 10)
-
+ "_almost_everywhere" :: "pttrn \<Rightarrow> 'a \<Rightarrow> bool \<Rightarrow> bool"
+ (\<open>(\<open>open_block notation=\<open>binder AE\<close>\<close>AE _ in _. _)\<close> [0,0,10] 10)
syntax_consts
"_almost_everywhere" \<rightleftharpoons> almost_everywhere
-
translations
"AE x in M. P" \<rightleftharpoons> "CONST almost_everywhere M (\<lambda>x. P)"
@@ -1017,11 +1016,9 @@
syntax
"_set_almost_everywhere" :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'a \<Rightarrow> bool \<Rightarrow> bool"
- (\<open>AE _\<in>_ in _./ _\<close> [0,0,0,10] 10)
-
+ (\<open>(\<open>open_block notation=\<open>binder AE\<close>\<close>AE _\<in>_ in _./ _)\<close> [0,0,0,10] 10)
syntax_consts
"_set_almost_everywhere" \<rightleftharpoons> set_almost_everywhere
-
translations
"AE x\<in>A in M. P" \<rightleftharpoons> "CONST set_almost_everywhere A M (\<lambda>x. P)"
--- a/src/HOL/Analysis/Nonnegative_Lebesgue_Integration.thy Wed Oct 09 22:01:33 2024 +0200
+++ b/src/HOL/Analysis/Nonnegative_Lebesgue_Integration.thy Wed Oct 09 23:38:29 2024 +0200
@@ -584,11 +584,10 @@
"integral\<^sup>S M f = (\<Sum>x \<in> f ` space M. x * emeasure M (f -` {x} \<inter> space M))"
syntax
- "_simple_integral" :: "pttrn \<Rightarrow> ennreal \<Rightarrow> 'a measure \<Rightarrow> ennreal" (\<open>\<integral>\<^sup>S _. _ \<partial>_\<close> [60,61] 110)
-
+ "_simple_integral" :: "pttrn \<Rightarrow> ennreal \<Rightarrow> 'a measure \<Rightarrow> ennreal"
+ (\<open>(\<open>open_block notation=\<open>binder integral\<close>\<close>\<integral>\<^sup>S _. _ \<partial>_)\<close> [60,61] 110)
syntax_consts
"_simple_integral" == simple_integral
-
translations
"\<integral>\<^sup>S x. f \<partial>M" == "CONST simple_integral M (%x. f)"
--- a/src/HOL/Analysis/Set_Integral.thy Wed Oct 09 22:01:33 2024 +0200
+++ b/src/HOL/Analysis/Set_Integral.thy Wed Oct 09 23:38:29 2024 +0200
@@ -577,21 +577,17 @@
syntax
"_complex_lebesgue_integral" :: "pttrn \<Rightarrow> complex \<Rightarrow> 'a measure \<Rightarrow> complex"
- (\<open>\<integral>\<^sup>C _. _ \<partial>_\<close> [0,0] 110)
-
+ (\<open>(\<open>open_block notation=\<open>binder integral\<close>\<close>\<integral>\<^sup>C _. _ \<partial>_)\<close> [0,0] 110)
syntax_consts
"_complex_lebesgue_integral" == complex_lebesgue_integral
-
translations
"\<integral>\<^sup>Cx. f \<partial>M" == "CONST complex_lebesgue_integral M (\<lambda>x. f)"
syntax
"_ascii_complex_lebesgue_integral" :: "pttrn \<Rightarrow> 'a measure \<Rightarrow> real \<Rightarrow> real"
(\<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
-
translations
"CLINT x|M. f" == "CONST complex_lebesgue_integral M (\<lambda>x. f)"
@@ -646,19 +642,16 @@
abbreviation "set_nn_integral M A f \<equiv> nn_integral M (\<lambda>x. f x * indicator A x)"
syntax
-"_set_nn_integral" :: "pttrn => 'a set => 'a measure => ereal => ereal"
-(\<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>(\<open>notation=\<open>binder integral\<close>\<close>\<integral>((_)\<in>(_)./ _)/\<partial>_)\<close> [0,0,0,110] 10)
-
+ "_set_nn_integral" :: "pttrn => 'a set => 'a measure => ereal => ereal"
+ (\<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>(\<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
-"_set_lebesgue_integral" == set_lebesgue_integral
-
+ "_set_nn_integral" == set_nn_integral and
+ "_set_lebesgue_integral" == set_lebesgue_integral
translations
-"\<integral>\<^sup>+x \<in> A. f \<partial>M" == "CONST set_nn_integral M A (\<lambda>x. f)"
-"\<integral>x \<in> A. f \<partial>M" == "CONST set_lebesgue_integral M A (\<lambda>x. f)"
+ "\<integral>\<^sup>+x \<in> A. f \<partial>M" == "CONST set_nn_integral M A (\<lambda>x. f)"
+ "\<integral>x \<in> A. f \<partial>M" == "CONST set_lebesgue_integral M A (\<lambda>x. f)"
lemma set_nn_integral_cong:
assumes "M = M'" "A = B" "\<And>x. x \<in> space M \<inter> A \<Longrightarrow> f x = g x"
--- a/src/HOL/Analysis/Starlike.thy Wed Oct 09 22:01:33 2024 +0200
+++ b/src/HOL/Analysis/Starlike.thy Wed Oct 09 23:38:29 2024 +0200
@@ -6414,7 +6414,7 @@
subsection\<open>Orthogonal complement\<close>
-definition\<^marker>\<open>tag important\<close> orthogonal_comp (\<open>_\<^sup>\<bottom>\<close> [80] 80)
+definition\<^marker>\<open>tag important\<close> orthogonal_comp (\<open>(\<open>open_block notation=\<open>postfix \<bottom>\<close>\<close>_\<^sup>\<bottom>)\<close> [80] 80)
where "orthogonal_comp W \<equiv> {x. \<forall>y \<in> W. orthogonal y x}"
proposition subspace_orthogonal_comp: "subspace (W\<^sup>\<bottom>)"
--- a/src/HOL/Library/Cardinality.thy Wed Oct 09 22:01:33 2024 +0200
+++ b/src/HOL/Library/Cardinality.thy Wed Oct 09 23:38:29 2024 +0200
@@ -30,7 +30,7 @@
subsection \<open>Cardinalities of types\<close>
-syntax "_type_card" :: "type => nat" (\<open>(1CARD/(1'(_')))\<close>)
+syntax "_type_card" :: "type => nat" (\<open>(\<open>indent=1 notation=\<open>mixfix CARD\<close>\<close>CARD/(1'(_')))\<close>)
syntax_consts "_type_card" == card
--- a/src/HOL/Library/FuncSet.thy Wed Oct 09 22:01:33 2024 +0200
+++ b/src/HOL/Library/FuncSet.thy Wed Oct 09 23:38:29 2024 +0200
@@ -28,8 +28,10 @@
end
syntax
- "_Pi" :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b set \<Rightarrow> ('a \<Rightarrow> 'b) set" (\<open>(3\<Pi> _\<in>_./ _)\<close> 10)
- "_lam" :: "pttrn \<Rightarrow> 'a set \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> ('a \<Rightarrow> 'b)" (\<open>(3\<lambda>_\<in>_./ _)\<close> [0,0,3] 3)
+ "_Pi" :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b set \<Rightarrow> ('a \<Rightarrow> 'b) set"
+ (\<open>(\<open>indent=3 notation=\<open>binder \<Pi>\<in>\<close>\<close>\<Pi> _\<in>_./ _)\<close> 10)
+ "_lam" :: "pttrn \<Rightarrow> 'a set \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> ('a \<Rightarrow> 'b)"
+ (\<open>(\<open>indent=3 notation=\<open>binder \<lambda>\<in>\<close>\<close>\<lambda>_\<in>_./ _)\<close> [0, 0, 3] 3)
syntax_consts
"_Pi" \<rightleftharpoons> Pi and
"_lam" \<rightleftharpoons> restrict
@@ -350,7 +352,8 @@
abbreviation "Pi\<^sub>E A B \<equiv> PiE A B"
syntax
- "_PiE" :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b set \<Rightarrow> ('a \<Rightarrow> 'b) set" (\<open>(3\<Pi>\<^sub>E _\<in>_./ _)\<close> 10)
+ "_PiE" :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b set \<Rightarrow> ('a \<Rightarrow> 'b) set"
+ (\<open>(\<open>indent=3 notation=\<open>binder \<Pi>\<^sub>E\<in>\<close>\<close>\<Pi>\<^sub>E _\<in>_./ _)\<close> 10)
syntax_consts
"_PiE" \<rightleftharpoons> Pi\<^sub>E
translations
--- a/src/HOL/Library/Going_To_Filter.thy Wed Oct 09 22:01:33 2024 +0200
+++ b/src/HOL/Library/Going_To_Filter.thy Wed Oct 09 23:38:29 2024 +0200
@@ -12,8 +12,8 @@
begin
definition going_to_within :: "('a \<Rightarrow> 'b) \<Rightarrow> 'b filter \<Rightarrow> 'a set \<Rightarrow> 'a filter"
- (\<open>(_)/ going'_to (_)/ within (_)\<close> [1000,60,60] 60) where
- "f going_to F within A = inf (filtercomap f F) (principal A)"
+ (\<open>(\<open>open_block notation=\<open>mixfix going_to_within\<close>\<close>(_)/ going'_to (_)/ within (_))\<close> [1000,60,60] 60)
+ where "f going_to F within A = inf (filtercomap f F) (principal A)"
abbreviation going_to :: "('a \<Rightarrow> 'b) \<Rightarrow> 'b filter \<Rightarrow> 'a filter"
(infix \<open>going'_to\<close> 60)
--- a/src/HOL/Library/Groups_Big_Fun.thy Wed Oct 09 22:01:33 2024 +0200
+++ b/src/HOL/Library/Groups_Big_Fun.thy Wed Oct 09 23:38:29 2024 +0200
@@ -199,9 +199,9 @@
end
syntax (ASCII)
- "_Sum_any" :: "pttrn \<Rightarrow> 'a \<Rightarrow> 'a::comm_monoid_add" (\<open>(3SUM _. _)\<close> [0, 10] 10)
+ "_Sum_any" :: "pttrn \<Rightarrow> 'a \<Rightarrow> 'a::comm_monoid_add" (\<open>(\<open>indent=3 notation=\<open>binder SUM\<close>\<close>SUM _. _)\<close> [0, 10] 10)
syntax
- "_Sum_any" :: "pttrn \<Rightarrow> 'a \<Rightarrow> 'a::comm_monoid_add" (\<open>(3\<Sum>_. _)\<close> [0, 10] 10)
+ "_Sum_any" :: "pttrn \<Rightarrow> 'a \<Rightarrow> 'a::comm_monoid_add" (\<open>(\<open>indent=2 notation=\<open>binder \<Sum>\<close>\<close>\<Sum>_. _)\<close> [0, 10] 10)
syntax_consts
"_Sum_any" \<rightleftharpoons> Sum_any
translations
@@ -254,9 +254,9 @@
end
syntax (ASCII)
- "_Prod_any" :: "pttrn \<Rightarrow> 'a \<Rightarrow> 'a::comm_monoid_mult" (\<open>(3PROD _. _)\<close> [0, 10] 10)
+ "_Prod_any" :: "pttrn \<Rightarrow> 'a \<Rightarrow> 'a::comm_monoid_mult" (\<open>(\<open>indent=4 notation=\<open>binder PROD\<close>\<close>PROD _. _)\<close> [0, 10] 10)
syntax
- "_Prod_any" :: "pttrn \<Rightarrow> 'a \<Rightarrow> 'a::comm_monoid_mult" (\<open>(3\<Prod>_. _)\<close> [0, 10] 10)
+ "_Prod_any" :: "pttrn \<Rightarrow> 'a \<Rightarrow> 'a::comm_monoid_mult" (\<open>(\<open>indent=2 notation=\<open>binder \<Prod>\<close>\<close>\<Prod>_. _)\<close> [0, 10] 10)
syntax_consts
"_Prod_any" == Prod_any
translations
--- a/src/HOL/Library/Interval.thy Wed Oct 09 22:01:33 2024 +0200
+++ b/src/HOL/Library/Interval.thy Wed Oct 09 23:38:29 2024 +0200
@@ -204,7 +204,7 @@
subsection \<open>Membership\<close>
-abbreviation (in preorder) in_interval (\<open>(_/ \<in>\<^sub>i _)\<close> [51, 51] 50)
+abbreviation (in preorder) in_interval (\<open>(\<open>notation=\<open>infix \<in>\<^sub>i\<close>\<close>_/ \<in>\<^sub>i _)\<close> [51, 51] 50)
where "in_interval x X \<equiv> x \<in> set_of X"
lemma in_interval_to_interval[intro!]: "a \<in>\<^sub>i interval_of a"
--- a/src/HOL/Library/Interval_Float.thy Wed Oct 09 22:01:33 2024 +0200
+++ b/src/HOL/Library/Interval_Float.thy Wed Oct 09 23:38:29 2024 +0200
@@ -92,8 +92,8 @@
"x \<in>\<^sub>i X" if "lower X \<le> x" "x \<le> upper X"
using that by (auto simp: set_of_eq)
-abbreviation in_real_interval (\<open>(_/ \<in>\<^sub>r _)\<close> [51, 51] 50) where
- "x \<in>\<^sub>r X \<equiv> x \<in>\<^sub>i real_interval X"
+abbreviation in_real_interval (\<open>(\<open>notation=\<open>infix \<in>\<^sub>r\<close>\<close>_/ \<in>\<^sub>r _)\<close> [51, 51] 50)
+ where "x \<in>\<^sub>r X \<equiv> x \<in>\<^sub>i real_interval X"
lemma in_real_intervalI:
"x \<in>\<^sub>r X" if "lower X \<le> x" "x \<le> upper X" for x::real and X::"float interval"
--- a/src/HOL/Library/Landau_Symbols.thy Wed Oct 09 22:01:33 2024 +0200
+++ b/src/HOL/Library/Landau_Symbols.thy Wed Oct 09 23:38:29 2024 +0200
@@ -26,39 +26,39 @@
\<close>
definition bigo :: "'a filter \<Rightarrow> ('a \<Rightarrow> ('b :: real_normed_field)) \<Rightarrow> ('a \<Rightarrow> 'b) set"
- (\<open>(1O[_]'(_'))\<close>)
+ (\<open>(\<open>indent=1 notation=\<open>mixfix bigo\<close>\<close>O[_]'(_'))\<close>)
where "bigo F g = {f. (\<exists>c>0. eventually (\<lambda>x. norm (f x) \<le> c * norm (g x)) F)}"
definition smallo :: "'a filter \<Rightarrow> ('a \<Rightarrow> ('b :: real_normed_field)) \<Rightarrow> ('a \<Rightarrow> 'b) set"
- (\<open>(1o[_]'(_'))\<close>)
+ (\<open>(\<open>indent=1 notation=\<open>mixfix smallo\<close>\<close>o[_]'(_'))\<close>)
where "smallo F g = {f. (\<forall>c>0. eventually (\<lambda>x. norm (f x) \<le> c * norm (g x)) F)}"
definition bigomega :: "'a filter \<Rightarrow> ('a \<Rightarrow> ('b :: real_normed_field)) \<Rightarrow> ('a \<Rightarrow> 'b) set"
- (\<open>(1\<Omega>[_]'(_'))\<close>)
+ (\<open>(\<open>indent=1 notation=\<open>mixfix bigomega\<close>\<close>\<Omega>[_]'(_'))\<close>)
where "bigomega F g = {f. (\<exists>c>0. eventually (\<lambda>x. norm (f x) \<ge> c * norm (g x)) F)}"
definition smallomega :: "'a filter \<Rightarrow> ('a \<Rightarrow> ('b :: real_normed_field)) \<Rightarrow> ('a \<Rightarrow> 'b) set"
- (\<open>(1\<omega>[_]'(_'))\<close>)
+ (\<open>(\<open>indent=1 notation=\<open>mixfix smallomega\<close>\<close>\<omega>[_]'(_'))\<close>)
where "smallomega F g = {f. (\<forall>c>0. eventually (\<lambda>x. norm (f x) \<ge> c * norm (g x)) F)}"
definition bigtheta :: "'a filter \<Rightarrow> ('a \<Rightarrow> ('b :: real_normed_field)) \<Rightarrow> ('a \<Rightarrow> 'b) set"
- (\<open>(1\<Theta>[_]'(_'))\<close>)
+ (\<open>(\<open>indent=1 notation=\<open>mixfix bigtheta\<close>\<close>\<Theta>[_]'(_'))\<close>)
where "bigtheta F g = bigo F g \<inter> bigomega F g"
-abbreviation bigo_at_top (\<open>(2O'(_'))\<close>) where
- "O(g) \<equiv> bigo at_top g"
+abbreviation bigo_at_top (\<open>(\<open>indent=2 notation=\<open>mixfix bigo\<close>\<close>O'(_'))\<close>)
+ where "O(g) \<equiv> bigo at_top g"
-abbreviation smallo_at_top (\<open>(2o'(_'))\<close>) where
- "o(g) \<equiv> smallo at_top g"
+abbreviation smallo_at_top (\<open>(\<open>indent=2 notation=\<open>mixfix smallo\<close>\<close>o'(_'))\<close>)
+ where "o(g) \<equiv> smallo at_top g"
-abbreviation bigomega_at_top (\<open>(2\<Omega>'(_'))\<close>) where
- "\<Omega>(g) \<equiv> bigomega at_top g"
+abbreviation bigomega_at_top (\<open>(\<open>indent=2 notation=\<open>mixfix bigomega\<close>\<close>\<Omega>'(_'))\<close>)
+ where "\<Omega>(g) \<equiv> bigomega at_top g"
-abbreviation smallomega_at_top (\<open>(2\<omega>'(_'))\<close>) where
- "\<omega>(g) \<equiv> smallomega at_top g"
+abbreviation smallomega_at_top (\<open>(\<open>indent=2 notation=\<open>mixfix smallomega\<close>\<close>\<omega>'(_'))\<close>)
+ where "\<omega>(g) \<equiv> smallomega at_top g"
-abbreviation bigtheta_at_top (\<open>(2\<Theta>'(_'))\<close>) where
- "\<Theta>(g) \<equiv> bigtheta at_top g"
+abbreviation bigtheta_at_top (\<open>(\<open>indent=2 notation=\<open>mixfix bigtheta\<close>\<close>\<Theta>'(_'))\<close>)
+ where "\<Theta>(g) \<equiv> bigtheta at_top g"
text \<open>The following is a set of properties that all Landau symbols satisfy.\<close>
@@ -1735,7 +1735,7 @@
named_theorems asymp_equiv_simps
definition asymp_equiv :: "('a \<Rightarrow> ('b :: real_normed_field)) \<Rightarrow> 'a filter \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> bool"
- (\<open>_ \<sim>[_] _\<close> [51, 10, 51] 50)
+ (\<open>(\<open>open_block notation=\<open>mixfix asymp_equiv\<close>\<close>_ \<sim>[_] _)\<close> [51, 10, 51] 50)
where "f \<sim>[F] g \<longleftrightarrow> ((\<lambda>x. if f x = 0 \<and> g x = 0 then 1 else f x / g x) \<longlongrightarrow> 1) F"
abbreviation (input) asymp_equiv_at_top where
--- a/src/HOL/Library/ListVector.thy Wed Oct 09 22:01:33 2024 +0200
+++ b/src/HOL/Library/ListVector.thy Wed Oct 09 23:38:29 2024 +0200
@@ -99,8 +99,8 @@
subsection "Inner product"
-definition iprod :: "'a::ring list \<Rightarrow> 'a list \<Rightarrow> 'a" (\<open>\<langle>_,_\<rangle>\<close>) where
-"\<langle>xs,ys\<rangle> = (\<Sum>(x,y) \<leftarrow> zip xs ys. x*y)"
+definition iprod :: "'a::ring list \<Rightarrow> 'a list \<Rightarrow> 'a" (\<open>(\<open>open_block notation=\<open>mixfix iprod\<close>\<close>\<langle>_,_\<rangle>)\<close>)
+ where "\<langle>xs,ys\<rangle> = (\<Sum>(x,y) \<leftarrow> zip xs ys. x*y)"
lemma iprod_Nil[simp]: "\<langle>[],ys\<rangle> = 0"
by(simp add: iprod_def)
--- a/src/HOL/Library/Multiset.thy Wed Oct 09 22:01:33 2024 +0200
+++ b/src/HOL/Library/Multiset.thy Wed Oct 09 23:38:29 2024 +0200
@@ -133,22 +133,22 @@
notation
member_mset (\<open>'(\<in>#')\<close>) and
- member_mset (\<open>(_/ \<in># _)\<close> [50, 51] 50)
+ member_mset (\<open>(\<open>notation=\<open>infix \<in>#\<close>\<close>_/ \<in># _)\<close> [50, 51] 50)
notation (ASCII)
member_mset (\<open>'(:#')\<close>) and
- member_mset (\<open>(_/ :# _)\<close> [50, 51] 50)
+ member_mset (\<open>(\<open>notation=\<open>infix :#\<close>\<close>_/ :# _)\<close> [50, 51] 50)
abbreviation not_member_mset :: \<open>'a \<Rightarrow> 'a multiset \<Rightarrow> bool\<close>
where \<open>not_member_mset a M \<equiv> a \<notin> set_mset M\<close>
notation
not_member_mset (\<open>'(\<notin>#')\<close>) and
- not_member_mset (\<open>(_/ \<notin># _)\<close> [50, 51] 50)
+ not_member_mset (\<open>(\<open>notation=\<open>infix \<notin>#\<close>\<close>_/ \<notin># _)\<close> [50, 51] 50)
notation (ASCII)
not_member_mset (\<open>'(~:#')\<close>) and
- not_member_mset (\<open>(_/ ~:# _)\<close> [50, 51] 50)
+ not_member_mset (\<open>(\<open>notation=\<open>infix ~:#\<close>\<close>_/ ~:# _)\<close> [50, 51] 50)
context
begin
@@ -162,17 +162,18 @@
end
syntax
- "_MBall" :: "pttrn \<Rightarrow> 'a set \<Rightarrow> bool \<Rightarrow> bool" (\<open>(3\<forall>_\<in>#_./ _)\<close> [0, 0, 10] 10)
- "_MBex" :: "pttrn \<Rightarrow> 'a set \<Rightarrow> bool \<Rightarrow> bool" (\<open>(3\<exists>_\<in>#_./ _)\<close> [0, 0, 10] 10)
-
+ "_MBall" :: "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)
+ "_MBex" :: "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)
syntax (ASCII)
- "_MBall" :: "pttrn \<Rightarrow> 'a set \<Rightarrow> bool \<Rightarrow> bool" (\<open>(3\<forall>_:#_./ _)\<close> [0, 0, 10] 10)
- "_MBex" :: "pttrn \<Rightarrow> 'a set \<Rightarrow> bool \<Rightarrow> bool" (\<open>(3\<exists>_:#_./ _)\<close> [0, 0, 10] 10)
-
+ "_MBall" :: "pttrn \<Rightarrow> 'a set \<Rightarrow> bool \<Rightarrow> bool"
+ (\<open>(\<open>indent=3 notation=\<open>binder \<forall>\<close>\<close>\<forall>_:#_./ _)\<close> [0, 0, 10] 10)
+ "_MBex" :: "pttrn \<Rightarrow> 'a set \<Rightarrow> bool \<Rightarrow> bool"
+ (\<open>(\<open>indent=3 notation=\<open>binder \<exists>\<close>\<close>\<exists>_:#_./ _)\<close> [0, 0, 10] 10)
syntax_consts
"_MBall" \<rightleftharpoons> Multiset.Ball and
"_MBex" \<rightleftharpoons> Multiset.Bex
-
translations
"\<forall>x\<in>#A. P" \<rightleftharpoons> "CONST Multiset.Ball A (\<lambda>x. P)"
"\<exists>x\<in>#A. P" \<rightleftharpoons> "CONST Multiset.Bex A (\<lambda>x. P)"
@@ -1249,9 +1250,11 @@
by (rule filter_preserves_multiset)
syntax (ASCII)
- "_MCollect" :: "pttrn \<Rightarrow> 'a multiset \<Rightarrow> bool \<Rightarrow> 'a multiset" (\<open>(1{#_ :# _./ _#})\<close>)
+ "_MCollect" :: "pttrn \<Rightarrow> 'a multiset \<Rightarrow> bool \<Rightarrow> 'a multiset"
+ (\<open>(\<open>indent=1 notation=\<open>mixfix multiset comprehension\<close>\<close>{#_ :# _./ _#})\<close>)
syntax
- "_MCollect" :: "pttrn \<Rightarrow> 'a multiset \<Rightarrow> bool \<Rightarrow> 'a multiset" (\<open>(1{#_ \<in># _./ _#})\<close>)
+ "_MCollect" :: "pttrn \<Rightarrow> 'a multiset \<Rightarrow> bool \<Rightarrow> 'a multiset"
+ (\<open>(\<open>indent=1 notation=\<open>mixfix multiset comprehension\<close>\<close>{#_ \<in># _./ _#})\<close>)
syntax_consts
"_MCollect" == filter_mset
translations
@@ -1824,18 +1827,22 @@
image_mset_subseteq_mono subset_mset.less_le_not_le)
syntax (ASCII)
- "_comprehension_mset" :: "'a \<Rightarrow> 'b \<Rightarrow> 'b multiset \<Rightarrow> 'a multiset" (\<open>({#_/. _ :# _#})\<close>)
+ "_comprehension_mset" :: "'a \<Rightarrow> 'b \<Rightarrow> 'b multiset \<Rightarrow> 'a multiset"
+ (\<open>(\<open>notation=\<open>mixfix multiset comprehension\<close>\<close>{#_/. _ :# _#})\<close>)
syntax
- "_comprehension_mset" :: "'a \<Rightarrow> 'b \<Rightarrow> 'b multiset \<Rightarrow> 'a multiset" (\<open>({#_/. _ \<in># _#})\<close>)
+ "_comprehension_mset" :: "'a \<Rightarrow> 'b \<Rightarrow> 'b multiset \<Rightarrow> 'a multiset"
+ (\<open>(\<open>notation=\<open>mixfix multiset comprehension\<close>\<close>{#_/. _ \<in># _#})\<close>)
syntax_consts
"_comprehension_mset" \<rightleftharpoons> image_mset
translations
"{#e. x \<in># M#}" \<rightleftharpoons> "CONST image_mset (\<lambda>x. e) M"
syntax (ASCII)
- "_comprehension_mset'" :: "'a \<Rightarrow> 'b \<Rightarrow> 'b multiset \<Rightarrow> bool \<Rightarrow> 'a multiset" (\<open>({#_/ | _ :# _./ _#})\<close>)
+ "_comprehension_mset'" :: "'a \<Rightarrow> 'b \<Rightarrow> 'b multiset \<Rightarrow> bool \<Rightarrow> 'a multiset"
+ (\<open>(\<open>notation=\<open>mixfix multiset comprehension\<close>\<close>{#_/ | _ :# _./ _#})\<close>)
syntax
- "_comprehension_mset'" :: "'a \<Rightarrow> 'b \<Rightarrow> 'b multiset \<Rightarrow> bool \<Rightarrow> 'a multiset" (\<open>({#_/ | _ \<in># _./ _#})\<close>)
+ "_comprehension_mset'" :: "'a \<Rightarrow> 'b \<Rightarrow> 'b multiset \<Rightarrow> bool \<Rightarrow> 'a multiset"
+ (\<open>(\<open>notation=\<open>mixfix multiset comprehension\<close>\<close>{#_/ | _ \<in># _./ _#})\<close>)
syntax_consts
"_comprehension_mset'" \<rightleftharpoons> image_mset
translations
@@ -2682,9 +2689,11 @@
notation sum_mset (\<open>\<Sum>\<^sub>#\<close>)
syntax (ASCII)
- "_sum_mset_image" :: "pttrn \<Rightarrow> 'b set \<Rightarrow> 'a \<Rightarrow> 'a::comm_monoid_add" (\<open>(3SUM _:#_. _)\<close> [0, 51, 10] 10)
+ "_sum_mset_image" :: "pttrn \<Rightarrow> 'b set \<Rightarrow> 'a \<Rightarrow> 'a::comm_monoid_add"
+ (\<open>(\<open>indent=3 notation=\<open>binder SUM\<close>\<close>SUM _:#_. _)\<close> [0, 51, 10] 10)
syntax
- "_sum_mset_image" :: "pttrn \<Rightarrow> 'b set \<Rightarrow> 'a \<Rightarrow> 'a::comm_monoid_add" (\<open>(3\<Sum>_\<in>#_. _)\<close> [0, 51, 10] 10)
+ "_sum_mset_image" :: "pttrn \<Rightarrow> 'b set \<Rightarrow> 'a \<Rightarrow> 'a::comm_monoid_add"
+ (\<open>(\<open>indent=3 notation=\<open>binder \<Sum>\<close>\<close>\<Sum>_\<in>#_. _)\<close> [0, 51, 10] 10)
syntax_consts
"_sum_mset_image" \<rightleftharpoons> sum_mset
translations
@@ -2863,9 +2872,11 @@
notation prod_mset (\<open>\<Prod>\<^sub>#\<close>)
syntax (ASCII)
- "_prod_mset_image" :: "pttrn \<Rightarrow> 'b set \<Rightarrow> 'a \<Rightarrow> 'a::comm_monoid_mult" (\<open>(3PROD _:#_. _)\<close> [0, 51, 10] 10)
+ "_prod_mset_image" :: "pttrn \<Rightarrow> 'b set \<Rightarrow> 'a \<Rightarrow> 'a::comm_monoid_mult"
+ (\<open>(\<open>indent=3 notation=\<open>binder PROD\<close>\<close>PROD _:#_. _)\<close> [0, 51, 10] 10)
syntax
- "_prod_mset_image" :: "pttrn \<Rightarrow> 'b set \<Rightarrow> 'a \<Rightarrow> 'a::comm_monoid_mult" (\<open>(3\<Prod>_\<in>#_. _)\<close> [0, 51, 10] 10)
+ "_prod_mset_image" :: "pttrn \<Rightarrow> 'b set \<Rightarrow> 'a \<Rightarrow> 'a::comm_monoid_mult"
+ (\<open>(\<open>indent=3 notation=\<open>binder \<Prod>\<close>\<close>\<Prod>_\<in>#_. _)\<close> [0, 51, 10] 10)
syntax_consts
"_prod_mset_image" \<rightleftharpoons> prod_mset
translations
--- a/src/HOL/Library/Omega_Words_Fun.thy Wed Oct 09 22:01:33 2024 +0200
+++ b/src/HOL/Library/Omega_Words_Fun.thy Wed Oct 09 23:38:29 2024 +0200
@@ -48,7 +48,7 @@
where "w \<frown> x == \<lambda>n. if n < length w then w!n else x (n - length w)"
definition
- iter :: "'a list \<Rightarrow> 'a word" (\<open>(_\<^sup>\<omega>)\<close> [1000])
+ iter :: "'a list \<Rightarrow> 'a word" (\<open>(\<open>notation=\<open>postfix \<omega>\<close>\<close>_\<^sup>\<omega>)\<close> [1000])
where "iter w == if w = [] then undefined else (\<lambda>n. w!(n mod (length w)))"
lemma conc_empty[simp]: "[] \<frown> w = w"
@@ -116,7 +116,8 @@
definition suffix :: "[nat, 'a word] \<Rightarrow> 'a word"
where "suffix k x \<equiv> \<lambda>n. x (k+n)"
-definition subsequence :: "'a word \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> 'a list" (\<open>_ [_ \<rightarrow> _]\<close> 900)
+definition subsequence :: "'a word \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> 'a list"
+ (\<open>(\<open>open_block notation=\<open>mixfix subsequence\<close>\<close>_ [_ \<rightarrow> _])\<close> 900)
where "subsequence w i j \<equiv> map w [i..<j]"
abbreviation prefix :: "nat \<Rightarrow> 'a word \<Rightarrow> 'a list"
--- a/src/HOL/Library/Phantom_Type.thy Wed Oct 09 22:01:33 2024 +0200
+++ b/src/HOL/Library/Phantom_Type.thy Wed Oct 09 23:38:29 2024 +0200
@@ -17,7 +17,7 @@
and of_phantom_comp_phantom [simp]: "of_phantom \<circ> phantom = id"
by(simp_all add: o_def id_def)
-syntax "_Phantom" :: "type \<Rightarrow> logic" (\<open>(1Phantom/(1'(_')))\<close>)
+syntax "_Phantom" :: "type \<Rightarrow> logic" (\<open>(\<open>indent=1 notation=\<open>mixfix Phantom\<close>\<close>Phantom/(1'(_')))\<close>)
syntax_consts "_Phantom" == phantom
translations
"Phantom('t)" => "CONST phantom :: _ \<Rightarrow> ('t, _) phantom"
--- a/src/HOL/Library/Preorder.thy Wed Oct 09 22:01:33 2024 +0200
+++ b/src/HOL/Library/Preorder.thy Wed Oct 09 23:38:29 2024 +0200
@@ -14,7 +14,7 @@
notation
equiv (\<open>'(\<approx>')\<close>) and
- equiv (\<open>(_/ \<approx> _)\<close> [51, 51] 50)
+ equiv (\<open>(\<open>notation=\<open>infix \<approx>\<close>\<close>_/ \<approx> _)\<close> [51, 51] 50)
lemma equivD1: "x \<le> y" if "x \<approx> y"
using that by (simp add: equiv_def)
--- a/src/HOL/Library/Quotient_Type.thy Wed Oct 09 22:01:33 2024 +0200
+++ b/src/HOL/Library/Quotient_Type.thy Wed Oct 09 23:38:29 2024 +0200
@@ -76,7 +76,7 @@
text \<open>Abstracted equivalence classes are the canonical representation of
elements of a quotient type.\<close>
-definition "class" :: "'a::equiv \<Rightarrow> 'a quot" (\<open>\<lfloor>_\<rfloor>\<close>)
+definition "class" :: "'a::equiv \<Rightarrow> 'a quot" (\<open>(\<open>open_block notation=\<open>mixfix class\<close>\<close>\<lfloor>_\<rfloor>)\<close>)
where "\<lfloor>a\<rfloor> = Abs_quot {x. a \<sim> x}"
theorem quot_exhaust: "\<exists>a. A = \<lfloor>a\<rfloor>"
--- a/src/HOL/Library/Ramsey.thy Wed Oct 09 22:01:33 2024 +0200
+++ b/src/HOL/Library/Ramsey.thy Wed Oct 09 23:38:29 2024 +0200
@@ -15,7 +15,7 @@
subsubsection \<open>The $n$-element subsets of a set $A$\<close>
-definition nsets :: "['a set, nat] \<Rightarrow> 'a set set" (\<open>([_]\<^bsup>_\<^esup>)\<close> [0,999] 999)
+definition nsets :: "['a set, nat] \<Rightarrow> 'a set set" (\<open>(\<open>notation=\<open>mixfix nsets\<close>\<close>[_]\<^bsup>_\<^esup>)\<close> [0,999] 999)
where "nsets A n \<equiv> {N. N \<subseteq> A \<and> finite N \<and> card N = n}"
lemma finite_imp_finite_nsets: "finite A \<Longrightarrow> finite ([A]\<^bsup>k\<^esup>)"
--- a/src/HOL/Library/Real_Mod.thy Wed Oct 09 22:01:33 2024 +0200
+++ b/src/HOL/Library/Real_Mod.thy Wed Oct 09 23:38:29 2024 +0200
@@ -106,8 +106,9 @@
-definition rcong :: "real \<Rightarrow> real \<Rightarrow> real \<Rightarrow> bool" (\<open>(1[_ = _] '(' rmod _'))\<close>) where
- "[x = y] (rmod m) \<longleftrightarrow> x rmod m = y rmod m"
+definition rcong :: "real \<Rightarrow> real \<Rightarrow> real \<Rightarrow> bool"
+ (\<open>(\<open>indent=1 notation=\<open>mixfix rcong\<close>\<close>[_ = _] '(' rmod _'))\<close>)
+ where "[x = y] (rmod m) \<longleftrightarrow> x rmod m = y rmod m"
named_theorems rcong_intros
--- a/src/HOL/Library/Tree.thy Wed Oct 09 22:01:33 2024 +0200
+++ b/src/HOL/Library/Tree.thy Wed Oct 09 23:38:29 2024 +0200
@@ -9,7 +9,7 @@
datatype 'a tree =
Leaf (\<open>\<langle>\<rangle>\<close>) |
- Node "'a tree" ("value": 'a) "'a tree" (\<open>(1\<langle>_,/ _,/ _\<rangle>)\<close>)
+ Node "'a tree" ("value": 'a) "'a tree" (\<open>(\<open>indent=1 notation=\<open>mixfix Node\<close>\<close>\<langle>_,/ _,/ _\<rangle>)\<close>)
datatype_compat tree
primrec left :: "'a tree \<Rightarrow> 'a tree" where
--- a/src/HOL/Library/Word.thy Wed Oct 09 22:01:33 2024 +0200
+++ b/src/HOL/Library/Word.thy Wed Oct 09 23:38:29 2024 +0200
@@ -1685,12 +1685,12 @@
notation
word_sle (\<open>'(\<le>s')\<close>) and
- word_sle (\<open>(_/ \<le>s _)\<close> [51, 51] 50) and
+ word_sle (\<open>(\<open>notation=\<open>infix \<le>s\<close>\<close>_/ \<le>s _)\<close> [51, 51] 50) and
word_sless (\<open>'(<s')\<close>) and
- word_sless (\<open>(_/ <s _)\<close> [51, 51] 50)
+ word_sless (\<open>(\<open>notation=\<open>infix <s\<close>\<close>_/ <s _)\<close> [51, 51] 50)
notation (input)
- word_sle (\<open>(_/ <=s _)\<close> [51, 51] 50)
+ word_sle (\<open>(\<open>notation=\<open>infix <=s\<close>\<close>_/ <=s _)\<close> [51, 51] 50)
lemma word_sle_eq [code]:
\<open>a <=s b \<longleftrightarrow> sint a \<le> sint b\<close>
--- a/src/HOL/Nonstandard_Analysis/HDeriv.thy Wed Oct 09 22:01:33 2024 +0200
+++ b/src/HOL/Nonstandard_Analysis/HDeriv.thy Wed Oct 09 23:38:29 2024 +0200
@@ -13,7 +13,7 @@
text \<open>Nonstandard Definitions.\<close>
definition nsderiv :: "['a::real_normed_field \<Rightarrow> 'a, 'a, 'a] \<Rightarrow> bool"
- (\<open>(NSDERIV (_)/ (_)/ :> (_))\<close> [1000, 1000, 60] 60)
+ (\<open>(\<open>notation=\<open>mixfix NSDERIV\<close>\<close>NSDERIV (_)/ (_)/ :> (_))\<close> [1000, 1000, 60] 60)
where "NSDERIV f x :> D \<longleftrightarrow>
(\<forall>h \<in> Infinitesimal - {0}. (( *f* f)(star_of x + h) - star_of (f x)) / h \<approx> star_of D)"
--- a/src/HOL/Nonstandard_Analysis/HLim.thy Wed Oct 09 22:01:33 2024 +0200
+++ b/src/HOL/Nonstandard_Analysis/HLim.thy Wed Oct 09 23:38:29 2024 +0200
@@ -13,7 +13,7 @@
text \<open>Nonstandard Definitions.\<close>
definition NSLIM :: "('a::real_normed_vector \<Rightarrow> 'b::real_normed_vector) \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> bool"
- (\<open>((_)/ \<midarrow>(_)/\<rightarrow>\<^sub>N\<^sub>S (_))\<close> [60, 0, 60] 60)
+ (\<open>(\<open>notation=\<open>mixfix NSLIM\<close>\<close>(_)/ \<midarrow>(_)/\<rightarrow>\<^sub>N\<^sub>S (_))\<close> [60, 0, 60] 60)
where "f \<midarrow>a\<rightarrow>\<^sub>N\<^sub>S L \<longleftrightarrow> (\<forall>x. x \<noteq> star_of a \<and> x \<approx> star_of a \<longrightarrow> ( *f* f) x \<approx> star_of L)"
definition isNSCont :: "('a::real_normed_vector \<Rightarrow> 'b::real_normed_vector) \<Rightarrow> 'a \<Rightarrow> bool"
--- a/src/HOL/Nonstandard_Analysis/HSEQ.thy Wed Oct 09 22:01:33 2024 +0200
+++ b/src/HOL/Nonstandard_Analysis/HSEQ.thy Wed Oct 09 23:38:29 2024 +0200
@@ -16,7 +16,7 @@
begin
definition NSLIMSEQ :: "(nat \<Rightarrow> 'a::real_normed_vector) \<Rightarrow> 'a \<Rightarrow> bool"
- (\<open>((_)/ \<longlonglongrightarrow>\<^sub>N\<^sub>S (_))\<close> [60, 60] 60) where
+ (\<open>(\<open>notation=\<open>mixfix NSLIMSEQ\<close>\<close>(_)/ \<longlonglongrightarrow>\<^sub>N\<^sub>S (_))\<close> [60, 60] 60) where
\<comment> \<open>Nonstandard definition of convergence of sequence\<close>
"X \<longlonglongrightarrow>\<^sub>N\<^sub>S L \<longleftrightarrow> (\<forall>N \<in> HNatInfinite. ( *f* X) N \<approx> star_of L)"
--- a/src/HOL/Nonstandard_Analysis/Star.thy Wed Oct 09 22:01:33 2024 +0200
+++ b/src/HOL/Nonstandard_Analysis/Star.thy Wed Oct 09 23:38:29 2024 +0200
@@ -11,7 +11,8 @@
begin
definition \<comment> \<open>internal sets\<close>
- starset_n :: "(nat \<Rightarrow> 'a set) \<Rightarrow> 'a star set" (\<open>*sn* _\<close> [80] 80)
+ starset_n :: "(nat \<Rightarrow> 'a set) \<Rightarrow> 'a star set"
+ (\<open>(\<open>open_block notation=\<open>prefix starset_n\<close>\<close>*sn* _)\<close> [80] 80)
where "*sn* As = Iset (star_n As)"
definition InternalSets :: "'a star set set"
@@ -23,7 +24,8 @@
(\<forall>x y. \<exists>X \<in> Rep_star x. \<exists>Y \<in> Rep_star y. y = F x \<longleftrightarrow> eventually (\<lambda>n. Y n = f(X n)) \<U>)"
definition \<comment> \<open>internal functions\<close>
- starfun_n :: "(nat \<Rightarrow> 'a \<Rightarrow> 'b) \<Rightarrow> 'a star \<Rightarrow> 'b star" (\<open>*fn* _\<close> [80] 80)
+ starfun_n :: "(nat \<Rightarrow> 'a \<Rightarrow> 'b) \<Rightarrow> 'a star \<Rightarrow> 'b star"
+ (\<open>(\<open>open_block notation=\<open>prefix starfun_n\<close>\<close>*fn* _)\<close> [80] 80)
where "*fn* F = Ifun (star_n F)"
definition InternalFuns :: "('a star => 'b star) set"
--- a/src/HOL/Nonstandard_Analysis/StarDef.thy Wed Oct 09 22:01:33 2024 +0200
+++ b/src/HOL/Nonstandard_Analysis/StarDef.thy Wed Oct 09 23:38:29 2024 +0200
@@ -72,7 +72,8 @@
by (simp add: FreeUltrafilterNat.proper)
text \<open>Standard principles that play a central role in the transfer tactic.\<close>
-definition Ifun :: "('a \<Rightarrow> 'b) star \<Rightarrow> 'a star \<Rightarrow> 'b star" (\<open>(_ \<star>/ _)\<close> [300, 301] 300)
+definition Ifun :: "('a \<Rightarrow> 'b) star \<Rightarrow> 'a star \<Rightarrow> 'b star"
+ (\<open>(\<open>notation=\<open>infix \<star>\<close>\<close>_ \<star>/ _)\<close> [300, 301] 300)
where "Ifun f \<equiv>
\<lambda>x. Abs_star (\<Union>F\<in>Rep_star f. \<Union>X\<in>Rep_star x. starrel``{\<lambda>n. F n (X n)})"
@@ -183,10 +184,12 @@
text \<open>Nonstandard extensions of functions.\<close>
-definition starfun :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a star \<Rightarrow> 'b star" (\<open>*f* _\<close> [80] 80)
+definition starfun :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a star \<Rightarrow> 'b star"
+ (\<open>(\<open>open_block notation=\<open>prefix starfun\<close>\<close>*f* _)\<close> [80] 80)
where "starfun f \<equiv> \<lambda>x. star_of f \<star> x"
-definition starfun2 :: "('a \<Rightarrow> 'b \<Rightarrow> 'c) \<Rightarrow> 'a star \<Rightarrow> 'b star \<Rightarrow> 'c star" (\<open>*f2* _\<close> [80] 80)
+definition starfun2 :: "('a \<Rightarrow> 'b \<Rightarrow> 'c) \<Rightarrow> 'a star \<Rightarrow> 'b star \<Rightarrow> 'c star"
+ (\<open>(\<open>open_block notation=\<open>prefix starfun2\<close>\<close>*f2* _)\<close> [80] 80)
where "starfun2 f \<equiv> \<lambda>x y. star_of f \<star> x \<star> y"
declare starfun_def [transfer_unfold]
@@ -270,10 +273,12 @@
lemma transfer_unstar [transfer_intro]: "p \<equiv> star_n P \<Longrightarrow> unstar p \<equiv> eventually P \<U>"
by (simp only: unstar_star_n)
-definition starP :: "('a \<Rightarrow> bool) \<Rightarrow> 'a star \<Rightarrow> bool" (\<open>*p* _\<close> [80] 80)
+definition starP :: "('a \<Rightarrow> bool) \<Rightarrow> 'a star \<Rightarrow> bool"
+ (\<open>(\<open>open_block notation=\<open>prefix starP\<close>\<close>*p* _)\<close> [80] 80)
where "*p* P = (\<lambda>x. unstar (star_of P \<star> x))"
-definition starP2 :: "('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> 'a star \<Rightarrow> 'b star \<Rightarrow> bool" (\<open>*p2* _\<close> [80] 80)
+definition starP2 :: "('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> 'a star \<Rightarrow> 'b star \<Rightarrow> bool"
+ (\<open>(\<open>open_block notation=\<open>prefix starP2\<close>\<close>*p2* _)\<close> [80] 80)
where "*p2* P = (\<lambda>x y. unstar (star_of P \<star> x \<star> y))"
declare starP_def [transfer_unfold]
@@ -332,7 +337,8 @@
text \<open>Nonstandard extensions of sets.\<close>
-definition starset :: "'a set \<Rightarrow> 'a star set" (\<open>*s* _\<close> [80] 80)
+definition starset :: "'a set \<Rightarrow> 'a star set"
+ (\<open>(\<open>open_block notation=\<open>prefix starset\<close>\<close>*s* _)\<close> [80] 80)
where "starset A = Iset (star_of A)"
declare starset_def [transfer_unfold]
--- a/src/HOL/Number_Theory/Cong.thy Wed Oct 09 22:01:33 2024 +0200
+++ b/src/HOL/Number_Theory/Cong.thy Wed Oct 09 23:38:29 2024 +0200
@@ -37,11 +37,13 @@
context unique_euclidean_semiring
begin
-definition cong :: "'a \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> bool" (\<open>(1[_ = _] '(' mod _'))\<close>)
- where "cong b c a \<longleftrightarrow> b mod a = c mod a"
+definition cong :: "'a \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> bool"
+ (\<open>(\<open>indent=1 notation=\<open>mixfix cong\<close>\<close>[_ = _] '(' mod _'))\<close>)
+ where "[b = c] (mod a) \<longleftrightarrow> b mod a = c mod a"
-abbreviation notcong :: "'a \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> bool" (\<open>(1[_ \<noteq> _] '(' mod _'))\<close>)
- where "notcong b c a \<equiv> \<not> cong b c a"
+abbreviation notcong :: "'a \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> bool"
+ (\<open>(\<open>indent=1 notation=\<open>mixfix notcong\<close>\<close>[_ \<noteq> _] '(' mod _'))\<close>)
+ where "[b \<noteq> c] (mod a) \<equiv> \<not> cong b c a"
lemma cong_refl [simp]:
"[b = b] (mod a)"
--- a/src/HOL/Probability/Fin_Map.thy Wed Oct 09 22:01:33 2024 +0200
+++ b/src/HOL/Probability/Fin_Map.thy Wed Oct 09 23:38:29 2024 +0200
@@ -13,7 +13,7 @@
stay close to the developments of (finite) products \<^const>\<open>Pi\<^sub>E\<close> and their sigma-algebra
\<^const>\<open>Pi\<^sub>M\<close>.\<close>
-type_notation fmap (\<open>(_ \<Rightarrow>\<^sub>F /_)\<close> [22, 21] 21)
+type_notation fmap (\<open>(\<open>notation=\<open>infix fmap\<close>\<close>_ \<Rightarrow>\<^sub>F /_)\<close> [22, 21] 21)
unbundle fmap.lifting
@@ -25,7 +25,8 @@
lemma finite_domain[simp, intro]: "finite (domain P)"
by transfer simp
-lift_definition proj :: "('i \<Rightarrow>\<^sub>F 'a) \<Rightarrow> 'i \<Rightarrow> 'a" (\<open>'((_)')\<^sub>F\<close> [0] 1000) is
+lift_definition proj :: "('i \<Rightarrow>\<^sub>F 'a) \<Rightarrow> 'i \<Rightarrow> 'a"
+ (\<open>(\<open>indent=1 notation=\<open>mixfix proj\<close>\<close>'(_')\<^sub>F)\<close> [0] 1000) is
"\<lambda>f x. if x \<in> dom f then the (f x) else undefined" .
declare [[coercion proj]]
@@ -89,7 +90,8 @@
"Pi' I A = { P. domain P = I \<and> (\<forall>i. i \<in> I \<longrightarrow> (P)\<^sub>F i \<in> A i) } "
syntax
- "_Pi'" :: "[pttrn, 'a set, 'b set] => ('a => 'b) set" (\<open>(3\<Pi>'' _\<in>_./ _)\<close> 10)
+ "_Pi'" :: "[pttrn, 'a set, 'b set] => ('a => 'b) set"
+ (\<open>(\<open>indent=3 notation=\<open>binder \<Pi>'\<close>\<close>\<Pi>'' _\<in>_./ _)\<close> 10)
syntax_consts
"_Pi'" == Pi'
translations
@@ -636,7 +638,8 @@
"Pi\<^sub>F I M \<equiv> PiF I M"
syntax
- "_PiF" :: "pttrn \<Rightarrow> 'i set \<Rightarrow> 'a measure \<Rightarrow> ('i => 'a) measure" (\<open>(3\<Pi>\<^sub>F _\<in>_./ _)\<close> 10)
+ "_PiF" :: "pttrn \<Rightarrow> 'i set \<Rightarrow> 'a measure \<Rightarrow> ('i => 'a) measure"
+ (\<open>(\<open>indent=3 notation=\<open>binder \<Pi>\<^sub>F\<close>\<close>\<Pi>\<^sub>F _\<in>_./ _)\<close> 10)
syntax_consts
"_PiF" == PiF
translations
--- a/src/HOL/Probability/SPMF.thy Wed Oct 09 22:01:33 2024 +0200
+++ b/src/HOL/Probability/SPMF.thy Wed Oct 09 23:38:29 2024 +0200
@@ -2621,8 +2621,9 @@
subsection \<open>Try\<close>
-definition try_spmf :: "'a spmf \<Rightarrow> 'a spmf \<Rightarrow> 'a spmf" (\<open>TRY _ ELSE _\<close> [0,60] 59)
-where "try_spmf p q = bind_pmf p (\<lambda>x. case x of None \<Rightarrow> q | Some y \<Rightarrow> return_spmf y)"
+definition try_spmf :: "'a spmf \<Rightarrow> 'a spmf \<Rightarrow> 'a spmf"
+ (\<open>(\<open>open_block notation=\<open>mixfix try_spmf\<close>\<close>TRY _ ELSE _)\<close> [0,60] 59)
+where "TRY p ELSE q = bind_pmf p (\<lambda>x. case x of None \<Rightarrow> q | Some y \<Rightarrow> return_spmf y)"
lemma try_spmf_lossless [simp]:
assumes "lossless_spmf p"
--- a/src/HOL/Unix/Unix.thy Wed Oct 09 22:01:33 2024 +0200
+++ b/src/HOL/Unix/Unix.thy Wed Oct 09 23:38:29 2024 +0200
@@ -336,7 +336,7 @@
\<close>
inductive transition :: "file \<Rightarrow> operation \<Rightarrow> file \<Rightarrow> bool"
- (\<open>_ \<midarrow>_\<rightarrow> _\<close> [90, 1000, 90] 100)
+ (\<open>(\<open>open_block notation=\<open>mixfix transition\<close>\<close>_ \<midarrow>_\<rightarrow> _)\<close> [90, 1000, 90] 100)
where
read:
"root \<midarrow>(Read uid text path)\<rightarrow> root"
@@ -475,7 +475,8 @@
running processes over a finite amount of time.
\<close>
-inductive transitions :: "file \<Rightarrow> operation list \<Rightarrow> file \<Rightarrow> bool" (\<open>_ \<Midarrow>_\<Rightarrow> _\<close> [90, 1000, 90] 100)
+inductive transitions :: "file \<Rightarrow> operation list \<Rightarrow> file \<Rightarrow> bool"
+ (\<open>(\<open>open_block notation=\<open>mixfix transitions\<close>\<close>_ \<Midarrow>_\<Rightarrow> _)\<close> [90, 1000, 90] 100)
where
nil: "root \<Midarrow>[]\<Rightarrow> root"
| cons: "root \<Midarrow>(x # xs)\<Rightarrow> root''" if "root \<midarrow>x\<rightarrow> root'" and "root' \<Midarrow>xs\<Rightarrow> root''"