# HG changeset patch
# User paulson
# Date 1077097229 -3600
# Node ID 386760e884626e5cd9b0711b69d90a4a1694331d
# Parent  bb726050650d060933a3fea7e4885a60814e6ece
removed obsolete theorem

diff -r bb726050650d -r 386760e88462 src/HOL/Real/RealPow.thy
--- 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";
 *}