| changeset 38767 | d8da44a8dd25 |
| parent 37216 | 3165bc303f66 |
| child 44048 | 64f574163ca2 |
| 38766:8891f4520d16 | 38767:d8da44a8dd25 |
|---|---|
1 theory Numbers |
1 theory Numbers |
2 imports Complex_Main |
2 imports Complex_Main |
3 begin |
3 begin |
4 |
4 |
5 ML "Pretty.margin_default := 64" |
5 ML "Pretty.margin_default := 64" |
6 ML "Thy_Output.indent := 0" (*we don't want 5 for listing theorems*) |
6 declare [[thy_output_indent = 0]] (*we don't want 5 for listing theorems*) |
7 |
7 |
8 text{* |
8 text{* |
9 |
9 |
10 numeric literals; default simprules; can re-orient |
10 numeric literals; default simprules; can re-orient |
11 *} |
11 *} |