| changeset 11234 | 6902638af59e |
| parent 11080 | 22855d091249 |
| child 16417 | 9bc16273c2d4 |
--- 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} *};