--- a/src/HOL/Divides.ML Tue Jun 12 14:11:00 2001 +0200
+++ b/src/HOL/Divides.ML Wed Jun 13 16:28:40 2001 +0200
@@ -505,6 +505,10 @@
(** Divides Relation **)
(************************************************)
+Goalw [dvd_def] "n = m * k \\<Longrightarrow> m dvd n";
+by (Blast_tac 1);
+qed "dvdI";
+
Goalw [dvd_def] "!!P. [|m dvd n; !!k. n = m*k ==> P|] ==> P";
by (Blast_tac 1);
qed "dvdE";
@@ -518,6 +522,11 @@
by Auto_tac;
qed "dvd_0_left";
+Goal "(0 dvd (m::nat)) = (m = 0)";
+by (blast_tac (claset() addIs [dvd_0_left]) 1);
+qed "dvd_0_left_iff";
+AddIffs [dvd_0_left_iff];
+
Goalw [dvd_def] "1 dvd (k::nat)";
by (Simp_tac 1);
qed "dvd_1_left";