\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: