--- a/src/HOL/Analysis/Cross3.thy Wed Oct 02 11:17:47 2024 +0200
+++ b/src/HOL/Analysis/Cross3.thy Wed Oct 02 11:27:19 2024 +0200
@@ -21,12 +21,14 @@
end
-bundle cross3_syntax begin
+bundle cross3_syntax
+begin
notation cross3 (infixr \<open>\<times>\<close> 80)
no_notation Product_Type.Times (infixr \<open>\<times>\<close> 80)
end
-bundle no_cross3_syntax begin
+bundle no_cross3_syntax
+begin
no_notation cross3 (infixr \<open>\<times>\<close> 80)
notation Product_Type.Times (infixr \<open>\<times>\<close> 80)
end
--- a/src/HOL/Analysis/Finite_Cartesian_Product.thy Wed Oct 02 11:17:47 2024 +0200
+++ b/src/HOL/Analysis/Finite_Cartesian_Product.thy Wed Oct 02 11:27:19 2024 +0200
@@ -20,16 +20,14 @@
declare vec_lambda_inject [simplified, simp]
-bundle vec_syntax begin
-notation
- vec_nth (infixl \<open>$\<close> 90) and
- vec_lambda (binder \<open>\<chi>\<close> 10)
+bundle vec_syntax
+begin
+notation vec_nth (infixl \<open>$\<close> 90) and vec_lambda (binder \<open>\<chi>\<close> 10)
end
-bundle no_vec_syntax begin
-no_notation
- vec_nth (infixl \<open>$\<close> 90) and
- vec_lambda (binder \<open>\<chi>\<close> 10)
+bundle no_vec_syntax
+begin
+no_notation vec_nth (infixl \<open>$\<close> 90) and vec_lambda (binder \<open>\<chi>\<close> 10)
end
unbundle vec_syntax
--- a/src/HOL/Analysis/Inner_Product.thy Wed Oct 02 11:17:47 2024 +0200
+++ b/src/HOL/Analysis/Inner_Product.thy Wed Oct 02 11:27:19 2024 +0200
@@ -461,11 +461,13 @@
lemmas has_derivative_norm = GDERIV_norm [unfolded gderiv_def]
-bundle inner_syntax begin
+bundle inner_syntax
+begin
notation inner (infix \<open>\<bullet>\<close> 70)
end
-bundle no_inner_syntax begin
+bundle no_inner_syntax
+begin
no_notation inner (infix \<open>\<bullet>\<close> 70)
end
--- a/src/HOL/Analysis/Lipschitz.thy Wed Oct 02 11:17:47 2024 +0200
+++ b/src/HOL/Analysis/Lipschitz.thy Wed Oct 02 11:27:19 2024 +0200
@@ -12,10 +12,12 @@
definition\<^marker>\<open>tag important\<close> lipschitz_on
where "lipschitz_on C U f \<longleftrightarrow> (0 \<le> C \<and> (\<forall>x \<in> U. \<forall>y\<in>U. dist (f x) (f y) \<le> C * dist x y))"
-bundle lipschitz_syntax begin
+bundle lipschitz_syntax
+begin
notation\<^marker>\<open>tag important\<close> lipschitz_on (\<open>_-lipschitz'_on\<close> [1000])
end
-bundle no_lipschitz_syntax begin
+bundle no_lipschitz_syntax
+begin
no_notation lipschitz_on (\<open>_-lipschitz'_on\<close> [1000])
end
--- a/src/HOL/Code_Evaluation.thy Wed Oct 02 11:17:47 2024 +0200
+++ b/src/HOL/Code_Evaluation.thy Wed Oct 02 11:27:19 2024 +0200
@@ -54,10 +54,7 @@
bundle term_syntax
begin
-
-notation App (infixl \<open><\<cdot>>\<close> 70)
- and valapp (infixl \<open>{\<cdot>}\<close> 70)
-
+notation App (infixl \<open><\<cdot>>\<close> 70) and valapp (infixl \<open>{\<cdot>}\<close> 70)
end
--- a/src/HOL/Combinatorics/Perm.thy Wed Oct 02 11:17:47 2024 +0200
+++ b/src/HOL/Combinatorics/Perm.thy Wed Oct 02 11:27:19 2024 +0200
@@ -794,16 +794,16 @@
bundle no_permutation_syntax
begin
- no_notation swap (\<open>\<langle>_ \<leftrightarrow> _\<rangle>\<close>)
- no_notation cycle (\<open>\<langle>_\<rangle>\<close>)
- no_notation "apply" (infixl \<open>\<langle>$\<rangle>\<close> 999)
+no_notation swap (\<open>\<langle>_ \<leftrightarrow> _\<rangle>\<close>)
+no_notation cycle (\<open>\<langle>_\<rangle>\<close>)
+no_notation "apply" (infixl \<open>\<langle>$\<rangle>\<close> 999)
end
bundle permutation_syntax
begin
- notation swap (\<open>\<langle>_ \<leftrightarrow> _\<rangle>\<close>)
- notation cycle (\<open>\<langle>_\<rangle>\<close>)
- notation "apply" (infixl \<open>\<langle>$\<rangle>\<close> 999)
+notation swap (\<open>\<langle>_ \<leftrightarrow> _\<rangle>\<close>)
+notation cycle (\<open>\<langle>_\<rangle>\<close>)
+notation "apply" (infixl \<open>\<langle>$\<rangle>\<close> 999)
end
unbundle no_permutation_syntax
--- a/src/HOL/Decision_Procs/Approximation.thy Wed Oct 02 11:17:47 2024 +0200
+++ b/src/HOL/Decision_Procs/Approximation.thy Wed Oct 02 11:27:19 2024 +0200
@@ -1143,7 +1143,8 @@
section "Avoid pollution of name space"
-bundle floatarith_notation begin
+bundle floatarith_notation
+begin
notation Add (\<open>Add\<close>)
notation Minus (\<open>Minus\<close>)
@@ -1166,7 +1167,8 @@
end
-bundle no_floatarith_notation begin
+bundle no_floatarith_notation
+begin
no_notation Add (\<open>Add\<close>)
no_notation Minus (\<open>Minus\<close>)
--- a/src/HOL/Product_Type.thy Wed Oct 02 11:17:47 2024 +0200
+++ b/src/HOL/Product_Type.thy Wed Oct 02 11:27:19 2024 +0200
@@ -803,10 +803,8 @@
bundle state_combinator_syntax
begin
-
notation fcomp (infixl \<open>\<circ>>\<close> 60)
notation scomp (infixl \<open>\<circ>\<rightarrow>\<close> 60)
-
end
context
@@ -1005,10 +1003,13 @@
where "A \<times> B \<equiv> Sigma A (\<lambda>_. B)"
end
-bundle no_Set_Product_syntax begin
+bundle no_Set_Product_syntax
+begin
no_notation Product_Type.Times (infixr \<open>\<times>\<close> 80)
end
-bundle Set_Product_syntax begin
+
+bundle Set_Product_syntax
+begin
notation Product_Type.Times (infixr \<open>\<times>\<close> 80)
end
--- a/src/HOL/Transfer.thy Wed Oct 02 11:17:47 2024 +0200
+++ b/src/HOL/Transfer.thy Wed Oct 02 11:27:19 2024 +0200
@@ -13,8 +13,8 @@
bundle lifting_syntax
begin
- notation rel_fun (infixr \<open>===>\<close> 55)
- notation map_fun (infixr \<open>--->\<close> 55)
+notation rel_fun (infixr \<open>===>\<close> 55)
+notation map_fun (infixr \<open>--->\<close> 55)
end
context includes lifting_syntax