| changeset 37695 | 71e84a203c19 |
| parent 37694 | 19e8b730ddeb |
| child 37696 | 1a6f475085fc |
| 37694:19e8b730ddeb | 37695:71e84a203c19 |
|---|---|
1 |
|
2 (* Author: Florian Haftmann, TU Muenchen *) |
|
3 |
|
4 header {* Generating code using pretty literals and natural number literals *} |
|
5 |
|
6 theory Codegenerator_Pretty |
|
7 imports "~~/src/HOL/ex/Codegenerator_Candidates" Code_Char Efficient_Nat |
|
8 begin |
|
9 |
|
10 declare isnorm.simps [code del] |
|
11 |
|
12 end |