diff -r 7eb63f63e6c6 -r 279da0358aa9 doc-src/TutorialI/Misc/prime_def.thy --- a/doc-src/TutorialI/Misc/prime_def.thy Thu Jul 26 16:43:02 2001 +0200 +++ b/doc-src/TutorialI/Misc/prime_def.thy Thu Jul 26 18:23:38 2001 +0200 @@ -1,6 +1,6 @@ (*<*) theory prime_def = Main:; -consts prime :: "nat \\ bool" +consts prime :: "nat \ bool" (*>*) text{* \begin{warn} @@ -8,6 +8,7 @@ variables on the right-hand side. Consider the following, flawed definition (where @{text"dvd"} 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"m"} on the right-hand side, which would introduce an inconsistency (why?). The correct version is