--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/TutorialI/Misc/document/prime_def.tex	Wed Apr 19 12:59:38 2000 +0200
@@ -0,0 +1,11 @@
+\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}%