doc-src/TutorialI/Misc/prime_def.thy

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/TutorialI/Misc/prime_def.thy	Wed Apr 19 11:56:31 2000 +0200
@@ -0,0 +1,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
+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
+should have written is
+*}
+(*<*)term(*>*)
+ "prime(p) \\<equiv> 1 < p \\<and> (\\<forall>m. (m dvd p) \\<longrightarrow> (m=1 \\<or> m=p))"
+(*<*)
+end
+(*>*)