--- a/doc-src/TutorialI/Misc/prime_def.thy Wed Jul 25 18:21:01 2001 +0200
+++ b/doc-src/TutorialI/Misc/prime_def.thy Thu Jul 26 16:43:02 2001 +0200
@@ -5,12 +5,12 @@
text{*
\begin{warn}
A common mistake when writing definitions is to introduce extra free
-variables on the right-hand side as in the following fictitious definition:
+variables on the right-hand side. Consider the following, flawed definition
+(where @{text"dvd"} means ``divides''):
@{term[display,quotes]"prime(p) == 1 < p & (m dvd p --> (m=1 | m=p))"}
-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
+right-hand side, which would introduce an inconsistency (why?).
+The correct version is
@{term[display,quotes]"prime(p) == 1 < p & (!m. m dvd p --> (m=1 | m=p))"}
\end{warn}
*}