--- 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 .
--- 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
--- 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)
--- 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