\begin{isabelle}%
\isanewline
\ \ \ \ {"}prime(p)\ {\isasymequiv}\ 1\ <\ p\ {\isasymand}\ (m\ dvd\ p\ {\isasymlongrightarrow}\ (m=1\ {\isasymor}\ m=p)){"}%
\begin{isamarkuptext}%
\noindent\small
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%
\end{isamarkuptext}%
\ {"}prime(p)\ {\isasymequiv}\ 1\ <\ p\ {\isasymand}\ ({\isasymforall}m.\ m\ dvd\ p\ {\isasymlongrightarrow}\ (m=1\ {\isasymor}\ m=p)){"}\end{isabelle}%
%%% Local Variables:
%%% mode: latex
%%% TeX-master: "root"
%%% End:
