# HG changeset patch
# User paulson <lp15@cam.ac.uk>
# Date 1529406852 -3600
# Node ID 44ffc5b9cd764c5ad40c7b4dde734bbc748d6e87
# Parent  3d8241f4198b9abee5d009e882faa532dcd78913
fixing overloading problems involving vector cross products

diff -r 3d8241f4198b -r 44ffc5b9cd76 src/HOL/Analysis/Cross3.thy
--- 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
 
diff -r 3d8241f4198b -r 44ffc5b9cd76 src/HOL/Product_Type.thy
--- 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