changeset 4891 | 19ff46cd2bad |
parent 4543 | 82a45bdd0e80 |
child 5369 | 8384e01b6cf8 |
4890:f0a24bad990a | 4891:19ff46cd2bad |
---|---|
118 ; |
118 ; |
119 |
119 |
120 defs : 'defs' (( id string ) + ) |
120 defs : 'defs' (( id string ) + ) |
121 ; |
121 ; |
122 |
122 |
123 constdefs : 'constdefs' (name '::' (string | type) string +) |
123 constdefs : 'constdefs' (name '::' (string | type) (() | mixfix) string +) |
124 ; |
124 ; |
125 |
125 |
126 axclass : 'axclass' classDecl (() | ( id string ) +) |
126 axclass : 'axclass' classDecl (() | ( id string ) +) |
127 ; |
127 ; |
128 |
128 |