# HG changeset patch
# User paulson
# Date 990267694 -7200
# Node ID 5a659c4064659fe9419b4d3830202b970704024f
# Parent  51e70b7bc315dab630dababd2040ce5702e3df62
power_le_dvd replaces power_less_dvd

diff -r 51e70b7bc315 -r 5a659c406465 src/HOL/Power.ML
--- a/src/HOL/Power.ML	Sat May 19 12:19:23 2001 +0200
+++ b/src/HOL/Power.ML	Sat May 19 12:21:34 2001 +0200
@@ -43,12 +43,11 @@
 by (contr_tac 1);
 qed "power_less_imp_less";
 
-Goal "k^j dvd n --> i<j --> k^i dvd (n::nat)";
+Goal "k^j dvd n --> i<=j --> k^i dvd (n::nat)";
 by (induct_tac "j" 1);
-by (ALLGOALS (simp_tac (simpset() addsimps [less_Suc_eq])));
-by (stac mult_commute 1);
-by (blast_tac (claset() addSDs [dvd_mult_left]) 1);
-qed_spec_mp "power_less_dvd";
+by (ALLGOALS (simp_tac (simpset() addsimps [le_Suc_eq])));
+by (blast_tac (claset() addSDs [dvd_mult_right]) 1);
+qed_spec_mp "power_le_dvd";
 
 
 (*** Binomial Coefficients, following Andy Gordon and Florian Kammueller ***)