31 Int :: ['a set, 'a set] => 'a set (infixl 70) |
31 Int :: ['a set, 'a set] => 'a set (infixl 70) |
32 Un :: ['a set, 'a set] => 'a set (infixl 65) |
32 Un :: ['a set, 'a set] => 'a set (infixl 65) |
33 UNION, INTER :: ['a set, 'a => 'b set] => 'b set (*general*) |
33 UNION, INTER :: ['a set, 'a => 'b set] => 'b set (*general*) |
34 Union, Inter :: (('a set) set) => 'a set (*of a set*) |
34 Union, Inter :: (('a set) set) => 'a set (*of a set*) |
35 Pow :: 'a set => 'a set set (*powerset*) |
35 Pow :: 'a set => 'a set set (*powerset*) |
36 range :: ('a => 'b) => 'b set (*of function*) |
|
37 Ball, Bex :: ['a set, 'a => bool] => bool (*bounded quantifiers*) |
36 Ball, Bex :: ['a set, 'a => bool] => bool (*bounded quantifiers*) |
38 "image" :: ['a => 'b, 'a set] => ('b set) (infixr "``" 90) |
37 "image" :: ['a => 'b, 'a set] => ('b set) (infixr "``" 90) |
39 (*membership*) |
38 (*membership*) |
40 "op :" :: ['a, 'a set] => bool ("(_/ : _)" [50, 51] 50) |
39 "op :" :: ['a, 'a set] => bool ("(_/ : _)" [50, 51] 50) |
41 |
40 |
42 |
41 |
43 (** Additional concrete syntax **) |
42 (** Additional concrete syntax **) |
44 |
43 |
45 syntax |
44 syntax |
|
45 range :: ('a => 'b) => 'b set (*of function*) |
46 |
46 |
47 (* Infix syntax for non-membership *) |
47 (* Infix syntax for non-membership *) |
48 |
48 |
49 "op ~:" :: ['a, 'a set] => bool ("op ~:") |
49 "op ~:" :: ['a, 'a set] => bool ("op ~:") |
50 "op ~:" :: ['a, 'a set] => bool ("(_/ ~: _)" [50, 51] 50) |
50 "op ~:" :: ['a, 'a set] => bool ("(_/ ~: _)" [50, 51] 50) |