Hide Product_Type.Times - too precious an identifier
authornipkow
Mon Nov 28 11:22:36 2011 +0100 (2011-11-28)
changeset 456624f7c05990420
parent 45657 862d68ee10f3
child 45663 d32ec2234efc
Hide Product_Type.Times - too precious an identifier
src/HOL/Product_Type.thy
     1.1 --- a/src/HOL/Product_Type.thy	Sun Nov 27 23:12:03 2011 +0100
     1.2 +++ b/src/HOL/Product_Type.thy	Mon Nov 28 11:22:36 2011 +0100
     1.3 @@ -897,6 +897,8 @@
     1.4  notation (HTML output)
     1.5    Times  (infixr "\<times>" 80)
     1.6  
     1.7 +hide_const (open) Times
     1.8 +
     1.9  syntax
    1.10    "_Sigma" :: "[pttrn, 'a set, 'b set] => ('a * 'b) set"  ("(3SIGMA _:_./ _)" [0, 0, 10] 10)
    1.11  translations