changeset 4991 | d7d525466221 |
parent 4986 | d4f257d3445a |
child 5004 | cf4e3b487caf |
4990:25da60d0a20b | 4991:d7d525466221 |
---|---|
14 |
14 |
15 |
15 |
16 (*basic utils*) |
16 (*basic utils*) |
17 use "library.ML"; |
17 use "library.ML"; |
18 use "table.ML"; |
18 use "table.ML"; |
19 use "object.ML"; |
|
19 use "seq.ML"; |
20 use "seq.ML"; |
20 use "name_space.ML"; |
21 use "name_space.ML"; |
21 use "term.ML"; |
22 use "term.ML"; |
22 |
23 |
23 (*inner syntax module*) |
24 (*inner syntax module*) |