(*<*) theory prime_def imports Main begin consts prime :: "nat ==> bool" (*>*) text‹
begin{warn}
common mistake when writing definitions is to introduce extra free
on the right-hand side. Consider the following, flawed definition
where ‹dvd› means ``divides''):
{term[display,quotes]"prime(p) ≡ 1 < p ∧ (m dvd p ⟶ (m=1 ∨ m=p))"}
par\noindent\hangindent=0pt
rejects this ``definition'' because of the extra term‹m› on the
-hand side, which would introduce an inconsistency (why?).
correct version is
{term[display,quotes]"prime(p) ≡ 1 < p ∧ (∀m. m dvd p ⟶ (m=1 ∨ m=p))"}
end{warn} › (*<*) end (*>*)
Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.
Bemerkung:
Die farbliche Syntaxdarstellung und die Messung sind noch experimentell.
