src/HOL/Power.thy
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