--- a/doc-src/TutorialI/Misc/prime_def.thy Tue Sep 05 13:12:00 2000 +0200
+++ b/doc-src/TutorialI/Misc/prime_def.thy Tue Sep 05 13:53:39 2000 +0200
@@ -2,17 +2,18 @@
theory prime_def = Main:;
consts prime :: "nat \\<Rightarrow> bool"
(*>*)
-(*<*)term(*>*)
-
- "prime(p) \\<equiv> 1 < p \\<and> (m dvd p \\<longrightarrow> (m=1 \\<or> m=p))";
-text{*\noindent\small
+text{*
+\begin{warn}
+A common mistake when writing definitions is to introduce extra free
+variables on the right-hand side as in the following fictitious definition:
+@{term[display,quotes]"prime(p) == 1 < p & (m dvd p --> (m=1 | m=p))"}
where @{text"dvd"} means ``divides''.
Isabelle rejects this ``definition'' because of the extra @{term"m"} on the
right-hand side, which would introduce an inconsistency (why?). What you
should have written is
+@{term[display,quotes]"prime(p) == 1 < p & (!m. m dvd p --> (m=1 | m=p))"}
+\end{warn}
*}
-(*<*)term(*>*)
- "prime(p) \\<equiv> 1 < p \\<and> (\\<forall>m. m dvd p \\<longrightarrow> (m=1 \\<or> m=p))"
(*<*)
end
(*>*)