1.1 --- a/src/HOL/Real/RealPow.thy	Tue Feb 17 17:41:30 2004 +0100
     1.2 +++ b/src/HOL/Real/RealPow.thy	Wed Feb 18 10:40:29 2004 +0100
     1.3 @@ -254,11 +254,6 @@
     1.4  apply (auto simp add: realpow_num_eq_if)
     1.5  done
     1.6  
     1.7 -(*???generalize the type!*)
     1.8 -lemma zero_le_x_squared [simp]: "(0::real) \<le> x^2"
     1.9 -by (simp add: power2_eq_square)
    1.10 -
    1.11 -
    1.12  
    1.13  ML
    1.14  {*
    1.15 @@ -315,7 +310,6 @@
    1.16  val realpow_num_eq_if = thm "realpow_num_eq_if";
    1.17  val real_num_zero_less_two_pow = thm "real_num_zero_less_two_pow";
    1.18  val lemma_realpow_num_two_mono = thm "lemma_realpow_num_two_mono";
    1.19 -val zero_le_x_squared = thm "zero_le_x_squared";
    1.20  *}
    1.21  
    1.22