# HG changeset patch
# User huffman
# Date 1182536379 -7200
# Node ID c869b52a9077500623842f0fbba6a9f9bc44aa2c
# Parent  688987d0bab484e45b4a3fc17c0809159043aeb1
reinstate real_root_less_iff [simp]

diff -r 688987d0bab4 -r c869b52a9077 src/HOL/Hyperreal/NthRoot.thy
--- a/src/HOL/Hyperreal/NthRoot.thy	Fri Jun 22 16:16:23 2007 +0200
+++ b/src/HOL/Hyperreal/NthRoot.thy	Fri Jun 22 20:19:39 2007 +0200
@@ -631,12 +631,4 @@
 lemma real_root_pos: "0 < x \<Longrightarrow> root (Suc n) (x ^ (Suc n)) = x"
 by (rule real_root_power_cancel [OF zero_less_Suc order_less_imp_le])
 
-(* FIXME: the stronger version of real_root_less_iff
- breaks CauchysMeanTheorem.list_gmean_gt_iff from AFP. *)
-
-declare real_root_less_iff [simp del]
-lemma real_root_less_iff_nonneg [simp]:
-  "\<lbrakk>0 < n; 0 \<le> x; 0 \<le> y\<rbrakk> \<Longrightarrow> (root n x < root n y) = (x < y)"
-by (rule real_root_less_iff)
-
 end