--- a/src/HOL/NSA/HyperDef.thy Tue Mar 04 14:14:28 2014 -0800
+++ b/src/HOL/NSA/HyperDef.thy Tue Mar 04 15:26:12 2014 -0800
@@ -346,7 +346,7 @@
K (Lin_Arith.add_inj_thms [@{thm star_of_le} RS iffD2,
@{thm star_of_less} RS iffD2, @{thm star_of_eq} RS iffD2]
#> Lin_Arith.add_simps [@{thm star_of_zero}, @{thm star_of_one},
- @{thm star_of_numeral}, @{thm star_of_neg_numeral}, @{thm star_of_add},
+ @{thm star_of_numeral}, @{thm star_of_add},
@{thm star_of_minus}, @{thm star_of_diff}, @{thm star_of_mult}]
#> Lin_Arith.add_inj_const (@{const_name "StarDef.star_of"}, @{typ "real \<Rightarrow> hypreal"}))
*}
@@ -496,9 +496,9 @@
"\<And>n. 1 pow n = (1::'a::monoid_mult star)"
by transfer (rule power_one)
-lemma hrabs_hyperpow_minus_one [simp]:
- "\<And>n. abs(-1 pow n) = (1::'a::{linordered_idom} star)"
-by transfer (rule abs_power_minus_one)
+lemma hrabs_hyperpow_minus [simp]:
+ "\<And>(a::'a::{linordered_idom} star) n. abs((-a) pow n) = abs (a pow n)"
+by transfer (rule abs_power_minus)
lemma hyperpow_mult:
"\<And>r s n. (r * s::'a::{comm_monoid_mult} star) pow n