# HG changeset patch
# User paulson
# Date 992442520 -7200
# Node ID ef11fb6e6c5894c32608f30c03c1ae895cd3a7b9
# Parent  648795477bb5f6c4a08f407da408bf7df7305f5b
a couple of new theorems

diff -r 648795477bb5 -r ef11fb6e6c58 src/HOL/Divides.ML
--- 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";