# HG changeset patch
# User huffman
# Date 1179023904 -7200
# Node ID 0b928312ab9462b6bc2a241c0c41513fe45b722d
# Parent  bf718970e5ef068200e435fe8f2d0872c0fa4512
removed redundant lemmas

diff -r bf718970e5ef -r 0b928312ab94 src/HOL/Hyperreal/NthRoot.thy
--- a/src/HOL/Hyperreal/NthRoot.thy	Sat May 12 18:16:30 2007 +0200
+++ b/src/HOL/Hyperreal/NthRoot.thy	Sun May 13 04:38:24 2007 +0200
@@ -329,9 +329,6 @@
 apply (erule real_sqrt_pow2)
 done
 
-lemma real_sqrt_abs_abs [simp]: "(sqrt \<bar>x\<bar>)\<twosuperior> = \<bar>x\<bar>" (* TODO: delete *)
-by simp
-
 lemma sqrt_eqI: "\<lbrakk>r\<twosuperior> = a; 0 \<le> r\<rbrakk> \<Longrightarrow> sqrt a = r"
 unfolding sqrt_def numeral_2_eq_2
 by (erule subst, erule real_root_pos2)
@@ -342,17 +339,6 @@
 apply (rule abs_ge_zero)
 done
 
-lemma real_pow_sqrt_eq_sqrt_pow: (* TODO: delete *)
-      "0 \<le> x ==> (sqrt x)\<twosuperior> = sqrt(x\<twosuperior>)"
-by simp
-
-lemma real_pow_sqrt_eq_sqrt_abs_pow2: (* TODO: delete *)
-     "0 \<le> x ==> (sqrt x)\<twosuperior> = sqrt(\<bar>x\<bar> ^ 2)" 
-by simp
-
-lemma real_sqrt_pow_abs: "0 \<le> x ==> (sqrt x)\<twosuperior> = \<bar>x\<bar>" (* TODO: delete *)
-by simp
-
 lemma not_real_square_gt_zero [simp]: "(~ (0::real) < x*x) = (x = 0)"
 apply auto
 apply (cut_tac x = x and y = 0 in linorder_less_linear)