changeset 48611 | b34ff75c23a7 |
parent 47183 | f760e15343bc |
48610:0095de9e9da0 | 48611:b34ff75c23a7 |
---|---|
1 theory Numbers |
1 theory Numbers |
2 imports Complex_Main |
2 imports Complex_Main |
3 begin |
3 begin |
4 |
|
5 ML "Pretty.margin_default := 64" |
|
6 declare [[thy_output_indent = 0]] (*we don't want 5 for listing theorems*) |
|
7 |
4 |
8 text{* |
5 text{* |
9 |
6 |
10 numeric literals; default simprules; can re-orient |
7 numeric literals; default simprules; can re-orient |
11 *} |
8 *} |