| changeset 2005 | 233bb805a4df |
| parent 1799 | 6471e252f14e |
| child 2380 | 41899210aafb |
| 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 |