changeset 48611 | b34ff75c23a7 |
parent 38767 | d8da44a8dd25 |
--- a/doc-src/TutorialI/Rules/Primes.thy Mon Jul 30 17:07:23 2012 +0200 +++ b/doc-src/TutorialI/Rules/Primes.thy Mon Jul 30 17:25:45 2012 +0200 @@ -8,10 +8,6 @@ "gcd m n = (if n=0 then m else gcd n (m mod n))" -ML "Pretty.margin_default := 64" -declare [[thy_output_indent = 5]] (*that is, Doc/TutorialI/settings.ML*) - - text {*Now in Basic.thy! @{thm[display]"dvd_def"} \rulename{dvd_def}