changeset 29933 | 125d513d9e39 |
parent 28663 | bd8438543bf2 |
child 31378 | d1cbf6393964 |
29932:a2594b5c945a | 29933:125d513d9e39 |
---|---|
1 (* Title: HOL/ex/Codegenerator_Pretty.thy |
1 (* Title: HOL/ex/Codegenerator_Pretty.thy |
2 ID: $Id$ |
|
3 Author: Florian Haftmann, TU Muenchen |
2 Author: Florian Haftmann, TU Muenchen |
4 *) |
3 *) |
5 |
4 |
6 header {* Simple examples for pretty numerals and such *} |
5 header {* Simple examples for pretty numerals and such *} |
7 |
6 |