changeset 36754 | 403585a89772 |
parent 33750 | 0a0d6d79d984 |
child 37216 | 3165bc303f66 |
1.1 --- a/doc-src/TutorialI/Types/Numbers.thy Sat May 08 16:53:53 2010 +0200 1.2 +++ b/doc-src/TutorialI/Types/Numbers.thy Sat May 08 19:14:13 2010 +0200 1.3 @@ -2,7 +2,7 @@ 1.4 imports Complex_Main 1.5 begin 1.6 1.7 -ML "Pretty.setmargin 64" 1.8 +ML "Pretty.margin_default := 64" 1.9 ML "ThyOutput.indent := 0" (*we don't want 5 for listing theorems*) 1.10 1.11 text{*