changeset 16796 | 140f1e0ea846 |
parent 16775 | c1b87ef4a1c3 |
child 17149 | e2b19c92ef51 |
--- a/src/HOL/Power.thy Wed Jul 13 15:06:04 2005 +0200 +++ b/src/HOL/Power.thy Wed Jul 13 15:06:20 2005 +0200 @@ -324,7 +324,7 @@ lemma le_imp_power_dvd: "!!i::nat. m \<le> n ==> i^m dvd i^n" apply (unfold dvd_def) -apply (erule not_less_iff_le [THEN iffD2, THEN add_diff_inverse, THEN subst]) +apply (erule linorder_not_less [THEN iffD2, THEN add_diff_inverse, THEN subst]) apply (simp add: power_add) done