(*<*) theory prime_def imports Main begin consts prime :: "nat \ bool" (*>*) text\<open> \begin{warn}
A common mistake when writing definitions isto introduce extra free
variables on the right-hand side. Consider the following, flawed definition
(where\<open>dvd\<close> means ``divides''):
@{term[display,quotes]"prime(p) \ 1 < p \ (m dvd p \ (m=1 \ m=p))"} \par\noindent\hangindent=0pt
Isabelle rejects this ``definition'' because of the extra \<^term>\<open>m\<close> on the
right-hand side, which would introduce an inconsistency (why?).
The correct version is
@{term[display,quotes]"prime(p) \ 1 < p \ (\m. m dvd p \ (m=1 \ m=p))"} \end{warn} \<close> (*<*) end (*>*)
¤ Dauer der Verarbeitung: 0.12 Sekunden
(vorverarbeitet)
¤
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 ist noch experimentell.
