| changeset 16417 | 9bc16273c2d4 |
| parent 15740 | d63e7a65b2d0 |
| child 16585 | 02cf78f0afce |
| 16416:6061ae1f90f2 | 16417:9bc16273c2d4 |
|---|---|
1 (* ID: $Id$ *) |
1 (* ID: $Id$ *) |
2 theory Numbers = Real: |
2 theory Numbers imports Real begin |
3 |
3 |
4 ML "Pretty.setmargin 64" |
4 ML "Pretty.setmargin 64" |
5 ML "IsarOutput.indent := 0" (*we don't want 5 for listing theorems*) |
5 ML "IsarOutput.indent := 0" (*we don't want 5 for listing theorems*) |
6 |
6 |
7 text{* |
7 text{* |