equal
deleted
inserted
replaced
162 (* |
162 (* |
163 "@Tuple" :: [i, is] => i ("\\<langle>(_,/ _)\\<rangle>") |
163 "@Tuple" :: [i, is] => i ("\\<langle>(_,/ _)\\<rangle>") |
164 "@pattern" :: patterns => pttrn ("\\<langle>_\\<rangle>") |
164 "@pattern" :: patterns => pttrn ("\\<langle>_\\<rangle>") |
165 *) |
165 *) |
166 |
166 |
|
167 syntax (HTML output) |
|
168 "op *" :: [i, i] => i (infixr "\\<times>" 80) |
|
169 |
167 |
170 |
168 defs |
171 defs |
169 |
172 |
170 (* Bounded Quantifiers *) |
173 (* Bounded Quantifiers *) |
171 Ball_def "Ball(A, P) == ALL x. x:A --> P(x)" |
174 Ball_def "Ball(A, P) == ALL x. x:A --> P(x)" |