--- a/doc-src/TutorialI/Misc/prime_def.thy Fri Jul 28 13:04:59 2000 +0200
+++ b/doc-src/TutorialI/Misc/prime_def.thy Fri Jul 28 16:02:51 2000 +0200
@@ -4,15 +4,15 @@
(*>*)
(*<*)term(*>*)
- "prime(p) \\<equiv> 1 < p \\<and> ((m dvd p) \\<longrightarrow> (m=1 \\<or> m=p))";
+ "prime(p) \\<equiv> 1 < p \\<and> (m dvd p \\<longrightarrow> (m=1 \\<or> m=p))";
text{*\noindent\small
where \isa{dvd} means ``divides''.
Isabelle rejects this ``definition'' because of the extra \isa{m} on the
-right-hand side, which would introduce an inconsistency. (Why?) What you
+right-hand side, which would introduce an inconsistency (why?). What you
should have written is
*}
(*<*)term(*>*)
- "prime(p) \\<equiv> 1 < p \\<and> (\\<forall>m. (m dvd p) \\<longrightarrow> (m=1 \\<or> m=p))"
+ "prime(p) \\<equiv> 1 < p \\<and> (\\<forall>m. m dvd p \\<longrightarrow> (m=1 \\<or> m=p))"
(*<*)
end
(*>*)