changeset 30161 | c26e515f1c29 |
parent 28663 | bd8438543bf2 |
child 30364 | 577edc39b501 |
30160:5f7b17941730 | 30161:c26e515f1c29 |
---|---|
1 (* Title: Tools/code/code_name.ML |
1 (* Title: Tools/code/code_name.ML |
2 ID: $Id$ |
|
3 Author: Florian Haftmann, TU Muenchen |
2 Author: Florian Haftmann, TU Muenchen |
4 |
3 |
5 Some code generator infrastructure concerning names. |
4 Some code generator infrastructure concerning names. |
6 *) |
5 *) |
7 |
6 |