author | nipkow |
Mon, 28 Nov 2011 18:08:07 +0100 | |
changeset 45663 | d32ec2234efc |
parent 45661 | ec6ba4b1f6d5 (current diff) |
parent 45662 | 4f7c05990420 (diff) |
child 45664 | ac6e704dcd12 |
--- 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