| changeset 2005 | 233bb805a4df |
| parent 1809 | 08e4d3cbcf8c |
| child 2033 | 74bd7bfb484b |
| 2004:b96e8cf86891 | 2005:233bb805a4df |
|---|---|
28 syntax (latex output) |
28 syntax (latex output) |
29 "_Collect" :: "pttrn => bool => 'a set" ("(1{_ . _})") |
29 "_Collect" :: "pttrn => bool => 'a set" ("(1{_ . _})") |
30 *) |
30 *) |
31 |
31 |
32 (* sort is used in Lists for sorting *) |
32 (* sort is used in Lists for sorting *) |
33 hide const sort |
33 hide_const sort |
34 |
34 |
35 abbreviation |
35 abbreviation |
36 "sort \<equiv> sort_of" |
36 "sort \<equiv> sort_of" |
37 |
37 |
38 abbreviation |
38 abbreviation |