src/HOL/Real/RealPow.thy
changeset 14392 386760e88462
parent 14387 e96d5c42c4b0
child 14443 75910c7557c5
--- 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";
 *}