--- 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 \\<Rightarrow> bool"
+consts prime :: "nat \<Rightarrow> 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