equal
deleted
inserted
replaced
15 subsection {* Basic syntax *} |
15 subsection {* Basic syntax *} |
16 |
16 |
17 global |
17 global |
18 |
18 |
19 typedecl 'a set |
19 typedecl 'a set |
20 arities set :: ("term") "term" |
20 arities set :: (type) type |
21 |
21 |
22 consts |
22 consts |
23 "{}" :: "'a set" ("{}") |
23 "{}" :: "'a set" ("{}") |
24 UNIV :: "'a set" |
24 UNIV :: "'a set" |
25 insert :: "'a => 'a set => 'a set" |
25 insert :: "'a => 'a set => 'a set" |
40 consts |
40 consts |
41 "op :" :: "'a => 'a set => bool" ("(_/ : _)" [50, 51] 50) -- "membership" |
41 "op :" :: "'a => 'a set => bool" ("(_/ : _)" [50, 51] 50) -- "membership" |
42 |
42 |
43 local |
43 local |
44 |
44 |
45 instance set :: ("term") ord .. |
45 instance set :: (type) ord .. |
46 instance set :: ("term") minus .. |
46 instance set :: (type) minus .. |
47 |
47 |
48 |
48 |
49 subsection {* Additional concrete syntax *} |
49 subsection {* Additional concrete syntax *} |
50 |
50 |
51 syntax |
51 syntax |