| changeset 22097 | 7ee0529c5674 |
| parent 16417 | 9bc16273c2d4 |
| child 25261 | 3dc292be0b54 |
--- a/doc-src/TutorialI/Rules/Primes.thy Fri Jan 19 22:08:03 2007 +0100 +++ b/doc-src/TutorialI/Rules/Primes.thy Fri Jan 19 22:08:04 2007 +0100 @@ -12,7 +12,7 @@ ML "Pretty.setmargin 64" -ML "IsarOutput.indent := 5" (*that is, Doc/TutorialI/settings.ML*) +ML "ThyOutput.indent := 5" (*that is, Doc/TutorialI/settings.ML*) text {*Now in Basic.thy!