doc-src/TutorialI/Rules/Primes.thy
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}