--- a/src/HOL/Real/RealPow.thy Tue Feb 17 17:41:30 2004 +0100
+++ b/src/HOL/Real/RealPow.thy Wed Feb 18 10:40:29 2004 +0100
@@ -254,11 +254,6 @@
apply (auto simp add: realpow_num_eq_if)
done
-(*???generalize the type!*)
-lemma zero_le_x_squared [simp]: "(0::real) \<le> x^2"
-by (simp add: power2_eq_square)
-
-
ML
{*
@@ -315,7 +310,6 @@
val realpow_num_eq_if = thm "realpow_num_eq_if";
val real_num_zero_less_two_pow = thm "real_num_zero_less_two_pow";
val lemma_realpow_num_two_mono = thm "lemma_realpow_num_two_mono";
-val zero_le_x_squared = thm "zero_le_x_squared";
*}