changeset 38767 | d8da44a8dd25 |
parent 37216 | 3165bc303f66 |
child 44048 | 64f574163ca2 |
--- a/doc-src/TutorialI/Types/Numbers.thy Fri Aug 27 00:09:56 2010 +0200 +++ b/doc-src/TutorialI/Types/Numbers.thy Fri Aug 27 12:40:20 2010 +0200 @@ -3,7 +3,7 @@ begin ML "Pretty.margin_default := 64" -ML "Thy_Output.indent := 0" (*we don't want 5 for listing theorems*) +declare [[thy_output_indent = 0]] (*we don't want 5 for listing theorems*) text{*