--- a/doc-src/TutorialI/Misc/document/prime_def.tex Wed Jul 25 18:21:01 2001 +0200
+++ b/doc-src/TutorialI/Misc/document/prime_def.tex Thu Jul 26 16:43:02 2001 +0200
@@ -5,14 +5,14 @@
\begin{isamarkuptext}%
\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 \isa{dvd} means ``divides''):
\begin{isabelle}%
\ \ \ \ \ {\isachardoublequote}prime\ p\ {\isasymequiv}\ {\isadigit{1}}\ {\isacharless}\ p\ {\isasymand}\ {\isacharparenleft}m\ dvd\ p\ {\isasymlongrightarrow}\ m\ {\isacharequal}\ {\isadigit{1}}\ {\isasymor}\ m\ {\isacharequal}\ p{\isacharparenright}{\isachardoublequote}%
\end{isabelle}
-where \isa{dvd} means ``divides''.
Isabelle rejects this ``definition'' because of the extra \isa{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
\begin{isabelle}%
\ \ \ \ \ {\isachardoublequote}prime\ p\ {\isasymequiv}\ {\isadigit{1}}\ {\isacharless}\ p\ {\isasymand}\ {\isacharparenleft}{\isasymforall}m{\isachardot}\ m\ dvd\ p\ {\isasymlongrightarrow}\ m\ {\isacharequal}\ {\isadigit{1}}\ {\isasymor}\ m\ {\isacharequal}\ p{\isacharparenright}{\isachardoublequote}%
\end{isabelle}