# HG changeset patch
# User huffman
# Date 1313880866 25200
# Node ID f057535311c588459492bc5d4b0b6963375e4dc2
# Parent  40101794c52f7ddcfe76bd73639af122886f2dcd
remove redundant lemma real_0_le_divide_iff in favor or zero_le_divide_iff

diff -r 40101794c52f -r f057535311c5 src/HOL/Decision_Procs/Approximation.thy
--- a/src/HOL/Decision_Procs/Approximation.thy	Sat Aug 20 13:07:00 2011 -0700
+++ b/src/HOL/Decision_Procs/Approximation.thy	Sat Aug 20 15:54:26 2011 -0700
@@ -712,7 +712,7 @@
         case False
         hence "real ?DIV \<le> 1" unfolding less_float_def by auto
 
-        have "0 \<le> x / ?R" using `0 \<le> real x` `0 < ?R` unfolding real_0_le_divide_iff by auto
+        have "0 \<le> x / ?R" using `0 \<le> real x` `0 < ?R` unfolding zero_le_divide_iff by auto
         hence "0 \<le> real ?DIV" using monotone by (rule order_trans)
 
         have "arctan x = 2 * arctan (x / ?R)" using arctan_half unfolding numeral_2_eq_2 power_Suc2 power_0 mult_1_left .
diff -r 40101794c52f -r f057535311c5 src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy
--- a/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy	Sat Aug 20 13:07:00 2011 -0700
+++ b/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy	Sat Aug 20 15:54:26 2011 -0700
@@ -1168,7 +1168,7 @@
       thus ?thesis unfolding obt1(5) obt2(5) unfolding * and ** using False
         apply(rule_tac x="((u * v1) / (u * v1 + v * v2)) *\<^sub>R b1 + ((v * v2) / (u * v1 + v * v2)) *\<^sub>R b2" in bexI) defer
         apply(rule convex_convex_hull[of s, unfolded convex_def, rule_format]) using obt1(4) obt2(4)
-        unfolding add_divide_distrib[THEN sym] and real_0_le_divide_iff
+        unfolding add_divide_distrib[THEN sym] and zero_le_divide_iff
         by (auto simp add: scaleR_left_distrib scaleR_right_distrib)
     qed note * = this
     have u1:"u1 \<le> 1" unfolding obt1(3)[THEN sym] and not_le using obt1(2) by auto
diff -r 40101794c52f -r f057535311c5 src/HOL/NthRoot.thy
--- a/src/HOL/NthRoot.thy	Sat Aug 20 13:07:00 2011 -0700
+++ b/src/HOL/NthRoot.thy	Sat Aug 20 15:54:26 2011 -0700
@@ -629,7 +629,7 @@
 apply (rule_tac y = "u/sqrt 2" in order_le_less_trans)
 apply (erule_tac [2] lemma_real_divide_sqrt_less)
 apply (rule power2_le_imp_le)
-apply (auto simp add: real_0_le_divide_iff power_divide)
+apply (auto simp add: zero_le_divide_iff power_divide)
 apply (rule_tac t = "u\<twosuperior>" in real_sum_of_halves [THEN subst])
 apply (rule add_mono)
 apply (auto simp add: four_x_squared intro: power_mono)
diff -r 40101794c52f -r f057535311c5 src/HOL/RealDef.thy
--- a/src/HOL/RealDef.thy	Sat Aug 20 13:07:00 2011 -0700
+++ b/src/HOL/RealDef.thy	Sat Aug 20 15:54:26 2011 -0700
@@ -1553,11 +1553,6 @@
 
 subsection{* Simprules combining x+y and 0: ARE THEY NEEDED?*}
 
-text{*Needed in this non-standard form by Hyperreal/Transcendental*}
-lemma real_0_le_divide_iff:
-     "((0::real) \<le> x/y) = ((x \<le> 0 | 0 \<le> y) & (0 \<le> x | y \<le> 0))"
-by (auto simp add: zero_le_divide_iff)
-
 lemma real_add_minus_iff [simp]: "(x + - a = (0::real)) = (x=a)" 
 by arith