diff -r 34c81a796ee3 -r 6902638af59e doc-src/TutorialI/Rules/Primes.thy
--- a/doc-src/TutorialI/Rules/Primes.thy	Fri Mar 30 12:31:10 2001 +0200
+++ b/doc-src/TutorialI/Rules/Primes.thy	Fri Mar 30 13:29:16 2001 +0200
@@ -15,11 +15,9 @@
 ML "IsarOutput.indent := 5"  (*that is, Doc/TutorialI/settings.ML*)
 
 
-text {*
-\begin{quote}
+text {*Now in Basic.thy!
 @{thm[display]"dvd_def"}
 \rulename{dvd_def}
-\end{quote}
 *};