diff -r a39e5d43de55 -r bbefb6ce5cb2 doc-src/TutorialI/Misc/prime_def.thy
--- a/doc-src/TutorialI/Misc/prime_def.thy	Fri Sep 01 18:29:52 2000 +0200
+++ b/doc-src/TutorialI/Misc/prime_def.thy	Fri Sep 01 19:09:44 2000 +0200
@@ -6,8 +6,8 @@
 
     "prime(p) \\<equiv> 1 < p \\<and> (m dvd p \\<longrightarrow> (m=1 \\<or> m=p))";
 text{*\noindent\small
-where \isa{dvd} means ``divides''.
-Isabelle rejects this ``definition'' because of the extra \isa{m} on the
+where @{text"dvd"} means ``divides''.
+Isabelle rejects this ``definition'' because of the extra @{term"m"} on the
 right-hand side, which would introduce an inconsistency (why?). What you
 should have written is
 *}