| changeset 27376 | ffe9b958bada |
| parent 23504 | 2b2323124e8e |
| child 27658 | 674496eb5965 |
| 27375:8d2c3d61c502 | 27376:ffe9b958bada |
|---|---|
1 (* ID: $Id$ *) |
1 (* ID: $Id$ *) |
2 theory Numbers imports Real begin |
2 theory Numbers |
3 imports Complex_Main |
|
4 begin |
|
3 |
5 |
4 ML "Pretty.setmargin 64" |
6 ML "Pretty.setmargin 64" |
5 ML "ThyOutput.indent := 0" (*we don't want 5 for listing theorems*) |
7 ML "ThyOutput.indent := 0" (*we don't want 5 for listing theorems*) |
6 |
8 |
7 text{* |
9 text{* |