src/HOL/Hyperreal/NthRoot.thy
changeset 23475 c869b52a9077
parent 23441 ee218296d635
child 23477 f4b83f03cac9
     1.1 --- a/src/HOL/Hyperreal/NthRoot.thy	Fri Jun 22 16:16:23 2007 +0200
     1.2 +++ b/src/HOL/Hyperreal/NthRoot.thy	Fri Jun 22 20:19:39 2007 +0200
     1.3 @@ -631,12 +631,4 @@
     1.4  lemma real_root_pos: "0 < x \<Longrightarrow> root (Suc n) (x ^ (Suc n)) = x"
     1.5  by (rule real_root_power_cancel [OF zero_less_Suc order_less_imp_le])
     1.6  
     1.7 -(* FIXME: the stronger version of real_root_less_iff
     1.8 - breaks CauchysMeanTheorem.list_gmean_gt_iff from AFP. *)
     1.9 -
    1.10 -declare real_root_less_iff [simp del]
    1.11 -lemma real_root_less_iff_nonneg [simp]:
    1.12 -  "\<lbrakk>0 < n; 0 \<le> x; 0 \<le> y\<rbrakk> \<Longrightarrow> (root n x < root n y) = (x < y)"
    1.13 -by (rule real_root_less_iff)
    1.14 -
    1.15  end