| changeset 36745 | 403585a89772 |
| parent 35416 | d8d7d1b785af |
| child 37216 | 3165bc303f66 |
--- a/doc-src/TutorialI/Rules/Primes.thy Sat May 08 16:53:53 2010 +0200 +++ b/doc-src/TutorialI/Rules/Primes.thy Sat May 08 19:14:13 2010 +0200 @@ -9,7 +9,7 @@ "gcd m n = (if n=0 then m else gcd n (m mod n))" -ML "Pretty.setmargin 64" +ML "Pretty.margin_default := 64" ML "ThyOutput.indent := 5" (*that is, Doc/TutorialI/settings.ML*)