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