| changeset 37216 | 3165bc303f66 |
| parent 36745 | 403585a89772 |
| child 38767 | d8da44a8dd25 |
--- a/doc-src/TutorialI/Rules/Primes.thy Mon May 31 19:36:13 2010 +0200 +++ b/doc-src/TutorialI/Rules/Primes.thy Mon May 31 21:06:57 2010 +0200 @@ -10,7 +10,7 @@ ML "Pretty.margin_default := 64" -ML "ThyOutput.indent := 5" (*that is, Doc/TutorialI/settings.ML*) +ML "Thy_Output.indent := 5" (*that is, Doc/TutorialI/settings.ML*) text {*Now in Basic.thy!