--- a/src/HOL/Analysis/Cross3.thy Fri Oct 04 00:00:50 2024 +0200
+++ b/src/HOL/Analysis/Cross3.thy Fri Oct 04 00:26:28 2024 +0200
@@ -10,7 +10,7 @@
imports Determinants Cartesian_Euclidean_Space
begin
-context includes no_Set_Product_syntax
+context includes no_set_product_syntax
begin \<comment>\<open>locally disable syntax for set product, to avoid warnings\<close>
definition\<^marker>\<open>tag important\<close> cross3 :: "[real^3, real^3] \<Rightarrow> real^3" (infixr \<open>\<times>\<close> 80)
@@ -21,20 +21,18 @@
end
-bundle cross3_syntax
+open_bundle cross3_syntax
begin
notation cross3 (infixr \<open>\<times>\<close> 80)
-no_notation Product_Type.Times (infixr \<open>\<times>\<close> 80)
+unbundle no_set_product_syntax
end
bundle no_cross3_syntax
begin
no_notation cross3 (infixr \<open>\<times>\<close> 80)
-notation Product_Type.Times (infixr \<open>\<times>\<close> 80)
+unbundle set_product_syntax
end
-unbundle cross3_syntax
-
subsection\<open> Basic lemmas\<close>
lemmas cross3_simps = cross3_def inner_vec_def sum_3 det_3 vec_eq_iff vector_def algebra_simps
--- a/src/HOL/Product_Type.thy Fri Oct 04 00:00:50 2024 +0200
+++ b/src/HOL/Product_Type.thy Fri Oct 04 00:26:28 2024 +0200
@@ -1003,16 +1003,16 @@
where "A \<times> B \<equiv> Sigma A (\<lambda>_. B)"
end
-bundle no_Set_Product_syntax
+bundle set_product_syntax
+begin
+notation Product_Type.Times (infixr \<open>\<times>\<close> 80)
+end
+
+bundle no_set_product_syntax
begin
no_notation Product_Type.Times (infixr \<open>\<times>\<close> 80)
end
-bundle Set_Product_syntax
-begin
-notation Product_Type.Times (infixr \<open>\<times>\<close> 80)
-end
-
syntax
"_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)