| changeset 22803 | 5129e02f4df2 |
| parent 22767 | 125363bf7518 |
| child 22949 | 997cef733bdd |
| 22802:92026479179e | 22803:5129e02f4df2 |
|---|---|
1 (* ID: $Id$ |
1 (* Title: HOL/Library/Pretty_Int.thy |
2 ID: $Id$ |
|
2 Author: Florian Haftmann, TU Muenchen |
3 Author: Florian Haftmann, TU Muenchen |
3 *) |
4 *) |
4 |
5 |
5 header {* Pretty integer literals for code generation *} |
6 header {* Pretty integer literals for code generation *} |
6 |
7 |