equal
deleted
inserted
replaced
45 instance set :: (type) "{ord, minus}" .. |
45 instance set :: (type) "{ord, minus}" .. |
46 |
46 |
47 |
47 |
48 subsection {* Additional concrete syntax *} |
48 subsection {* Additional concrete syntax *} |
49 |
49 |
50 abbreviation (output) |
50 abbreviation |
51 range :: "('a => 'b) => 'b set" -- "of function" |
51 range :: "('a => 'b) => 'b set" -- "of function" |
52 "range f = f ` UNIV" |
52 "range f == f ` UNIV" |
53 |
53 |
54 syntax |
54 syntax |
55 "op ~:" :: "'a => 'a set => bool" ("op ~:") -- "non-membership" |
55 "op ~:" :: "'a => 'a set => bool" ("op ~:") -- "non-membership" |
56 "op ~:" :: "'a => 'a set => bool" ("(_/ ~: _)" [50, 51] 50) |
56 "op ~:" :: "'a => 'a set => bool" ("(_/ ~: _)" [50, 51] 50) |
57 |
57 |