equal
deleted
inserted
replaced
1 (* Title: Pure/Tools/codegen_names.ML |
1 (* Title: Pure/Tools/codegen_names.ML |
2 ID: $Id$ |
2 ID: $Id$ |
3 Author: Florian Haftmann, TU Muenchen |
3 Author: Florian Haftmann, TU Muenchen |
4 |
4 |
5 Name policies for code generation: prefixing any name by corresponding theory name, |
5 Name policies for code generation: prefixing any name by corresponding theory name, |
6 conversion to alphanumeric representation. Mappings are incrementally cached. |
6 conversion to alphanumeric representation, shallow name spaces. |
|
7 Mappings are incrementally cached. |
7 *) |
8 *) |
8 |
9 |
9 signature CODEGEN_NAMES = |
10 signature CODEGEN_NAMES = |
10 sig |
11 sig |
11 type tyco = string |
12 type tyco = string |