--- a/src/HOL/Analysis/Cross3.thy Mon Jun 18 15:56:03 2018 +0100
+++ b/src/HOL/Analysis/Cross3.thy Tue Jun 19 12:14:12 2018 +0100
@@ -10,12 +10,29 @@
imports Determinants
begin
+context includes no_Set_Product_syntax
+begin \<comment>\<open>locally disable syntax for set product, to avoid warnings\<close>
+
definition cross3 :: "[real^3, real^3] \<Rightarrow> real^3" (infixr "\<times>" 80)
where "a \<times> b \<equiv>
vector [a$2 * b$3 - a$3 * b$2,
a$3 * b$1 - a$1 * b$3,
a$1 * b$2 - a$2 * b$1]"
+end
+
+bundle cross3_syntax begin
+notation cross3 (infixr "\<times>" 80)
+no_notation Product_Type.Times (infixr "\<times>" 80)
+end
+
+bundle no_cross3_syntax begin
+no_notation cross3 (infixr "\<times>" 80)
+notation Product_Type.Times (infixr "\<times>" 80)
+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
@@ -60,6 +77,8 @@
lemma right_diff_distrib: "x \<times> (y - z) = x \<times> y - x \<times> z" for x::"real^3"
by (simp add: cross3_simps)
+hide_fact (open) left_diff_distrib right_diff_distrib
+
lemma Jacobi: "x \<times> (y \<times> z) + y \<times> (z \<times> x) + z \<times> (x \<times> y) = 0" for x::"real^3"
by (simp add: cross3_simps)
@@ -202,5 +221,7 @@
shows "\<lbrakk>continuous_on S f; continuous_on S g\<rbrakk> \<Longrightarrow> continuous_on S (\<lambda>x. (f x) \<times> (g x))"
by (simp add: continuous_on_eq_continuous_within continuous_cross)
+unbundle no_cross3_syntax
+
end
--- a/src/HOL/Product_Type.thy Mon Jun 18 15:56:03 2018 +0100
+++ b/src/HOL/Product_Type.thy Tue Jun 19 12:14:12 2018 +0100
@@ -963,6 +963,13 @@
hide_const (open) Times
+bundle no_Set_Product_syntax begin
+no_notation Product_Type.Times (infixr "\<times>" 80)
+end
+bundle Set_Product_syntax begin
+notation Product_Type.Times (infixr "\<times>" 80)
+end
+
syntax
"_Sigma" :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b set \<Rightarrow> ('a \<times> 'b) set" ("(3SIGMA _:_./ _)" [0, 0, 10] 10)
translations