--- 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
*}