merged
authornipkow
Mon, 28 Nov 2011 18:08:07 +0100
changeset 45663 d32ec2234efc
parent 45661 ec6ba4b1f6d5 (current diff)
parent 45662 4f7c05990420 (diff)
child 45664 ac6e704dcd12
merged
--- a/src/HOL/Product_Type.thy	Mon Nov 28 17:06:29 2011 +0100
+++ b/src/HOL/Product_Type.thy	Mon Nov 28 18:08:07 2011 +0100
@@ -897,6 +897,8 @@
 notation (HTML output)
   Times  (infixr "\<times>" 80)
 
+hide_const (open) Times
+
 syntax
   "_Sigma" :: "[pttrn, 'a set, 'b set] => ('a * 'b) set"  ("(3SIGMA _:_./ _)" [0, 0, 10] 10)
 translations