equal
deleted
inserted
replaced
29 Pow :: 'a set => 'a set set (*powerset*) |
29 Pow :: 'a set => 'a set set (*powerset*) |
30 range :: ('a => 'b) => 'b set (*of function*) |
30 range :: ('a => 'b) => 'b set (*of function*) |
31 Ball, Bex :: ['a set, 'a => bool] => bool (*bounded quantifiers*) |
31 Ball, Bex :: ['a set, 'a => bool] => bool (*bounded quantifiers*) |
32 inj, surj :: ('a => 'b) => bool (*inj/surjective*) |
32 inj, surj :: ('a => 'b) => bool (*inj/surjective*) |
33 inj_onto :: ['a => 'b, 'a set] => bool |
33 inj_onto :: ['a => 'b, 'a set] => bool |
34 "``" :: ['a => 'b, 'a set] => ('b set) (infixl 90) |
34 "``" :: ['a => 'b, 'a set] => ('b set) (infixr 90) |
35 ":" :: ['a, 'a set] => bool (infixl 50) (*membership*) |
35 ":" :: ['a, 'a set] => bool (infixl 50) (*membership*) |
36 |
36 |
37 |
37 |
38 syntax |
38 syntax |
39 |
39 |