changeset 45605 | a89b4bc311a5 |
parent 45542 | 4849dbe6e310 |
child 47108 | 2a1953f0d20d |
--- a/src/HOL/NSA/HyperDef.thy Sun Nov 20 20:59:30 2011 +0100 +++ b/src/HOL/NSA/HyperDef.thy Sun Nov 20 21:05:23 2011 +0100 @@ -422,7 +422,7 @@ lemma power_hypreal_of_real_number_of: "(number_of v :: hypreal) ^ n = hypreal_of_real ((number_of v) ^ n)" by simp -declare power_hypreal_of_real_number_of [of _ "number_of w", standard, simp] +declare power_hypreal_of_real_number_of [of _ "number_of w", simp] for w (* lemma hrealpow_HFinite: fixes x :: "'a::{real_normed_algebra,power} star"