--- a/src/HOL/Analysis/Cross3.thy Fri Sep 20 19:07:10 2024 +0200
+++ b/src/HOL/Analysis/Cross3.thy Fri Sep 20 19:51:08 2024 +0200
@@ -13,7 +13,7 @@
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 "\<times>" 80)
+definition\<^marker>\<open>tag important\<close> cross3 :: "[real^3, real^3] \<Rightarrow> real^3" (infixr \<open>\<times>\<close> 80)
where "a \<times> b \<equiv>
vector [a$2 * b$3 - a$3 * b$2,
a$3 * b$1 - a$1 * b$3,
@@ -22,13 +22,13 @@
end
bundle cross3_syntax begin
-notation cross3 (infixr "\<times>" 80)
-no_notation Product_Type.Times (infixr "\<times>" 80)
+notation cross3 (infixr \<open>\<times>\<close> 80)
+no_notation Product_Type.Times (infixr \<open>\<times>\<close> 80)
end
bundle no_cross3_syntax begin
-no_notation cross3 (infixr "\<times>" 80)
-notation Product_Type.Times (infixr "\<times>" 80)
+no_notation cross3 (infixr \<open>\<times>\<close> 80)
+notation Product_Type.Times (infixr \<open>\<times>\<close> 80)
end
unbundle cross3_syntax