--- a/src/HOL/Hyperreal/HyperPow.thy Tue Jul 26 18:31:18 2005 +0200
+++ b/src/HOL/Hyperreal/HyperPow.thy Wed Jul 27 11:28:18 2005 +0200
@@ -68,10 +68,11 @@
(x = 0 & y = 0 & z = 0)"
by (simp only: hypreal_three_squares_add_zero_iff hrealpow_two)
-
+(*FIXME: This and RealPow.abs_realpow_two should be replaced by an abstract
+ result proved in Ring_and_Field*)
lemma hrabs_hrealpow_two [simp]:
"abs(x ^ Suc (Suc 0)) = (x::hypreal) ^ Suc (Suc 0)"
-by (simp)
+by (simp add: abs_mult)
lemma two_hrealpow_ge_one [simp]: "(1::hypreal) \<le> 2 ^ n"
by (insert power_increasing [of 0 n "2::hypreal"], simp)