--- 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