diff -r 0095de9e9da0 -r b34ff75c23a7 doc-src/TutorialI/Types/Numbers.thy --- a/doc-src/TutorialI/Types/Numbers.thy Mon Jul 30 17:07:23 2012 +0200 +++ b/doc-src/TutorialI/Types/Numbers.thy Mon Jul 30 17:25:45 2012 +0200 @@ -2,9 +2,6 @@ imports Complex_Main begin -ML "Pretty.margin_default := 64" -declare [[thy_output_indent = 0]] (*we don't want 5 for listing theorems*) - text{* numeric literals; default simprules; can re-orient