Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
power_le_dvd replaces power_less_dvd
authorpaulson
Sat, 19 May 2001 12:21:34 +0200
changeset 11311 5a659c406465
parent 11310 51e70b7bc315
child 11312 4104bd8d1528
power_le_dvd replaces power_less_dvd
src/HOL/Power.ML file | annotate | diff | comparison | revisions 
--- 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 ***)
isabelle