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