Rigorous definition of integration of hyperreal functions? Motivated by this question, I am curious to see whether the Dirac delta function could be represented with a hyperreal function using the following "hyperreal Gaussian:"
$$\delta(x)=\sqrt{\frac{H}{\pi}}\,e^{-Hx^2},$$
where $H$ is a positive infinite (hyperreal) number. It seems natural to expect that 
$$\int_{-\infty}^{+\infty}\delta(x)\,dx = 1,$$
as this is true if we replace $H$ with any positive finite real number. Nonetheless, to prove this, we would need (or at any rate, I would like to know) a rigorous definition of integration for hyperreal functions. 
What is the/a rigorous way to define integration over hyperreal functions, and how can we use this to prove the above integral identity?

As a side note I'll add that I tried using Keisler's definition in "Calculus, An Infinitesimal Approach," but his definition only seems to apply to real-valued continuous functions, which rules out this delta function since it is infinite near $x=0$. Even if we use his definition anyway, it is unclear whether it would give a sensible answer.
His definition is
$$\int_a^b f(x)\,dx:= st\left(\sum_a^b f(x)\,dx \right),$$
where $dx$ is infinitesimal and the sum has an infinite number of terms.
 A: If you define the hyperreals as an ultrapower of the reals, there is absolutely no difficulty talking about integrals of internal functions.  An internal function is any function that is given by a sequence of functions $\mathbb{R}\to\mathbb{R}$, evaluated on the hyperreals by termwise evaluation (thinking of hyperreals as equivalence classes of sequences of reals).  The integral is then defined by just integrating each coordinate to get a sequence of reals and hence a hyperreal (of course, for this to make sense, you need all or almost all of the coordinates to be integrable functions).  Another way to say this is that you can take an ultrapower of not just the reals but of a larger structure which includes higher-order functions on the reals, and in particular includes the integration operator.
In your case, your $\delta$ would be the internal function defined by the sequence of functions $\delta_n(x)=\sqrt{H_n/\pi}e^{-H_nx^2}$ where $(H_n)$ is a sequence representing the hyperreal $H$.  Its integral is $1$ since the integral of each $\delta_n$ is $1$.  Similarly, for any standard function $f$, the integral $\int_{-\infty}^\infty f\delta$ would just by definition be the hyperreal defined by the sequence $\int_{-\infty}^\infty f\delta_n$, so in particular it would be infinitesimally close to $f(0)$ if $f$ is bounded and continuous.  If you want to get a real number rather than a hyperreal as the output of your integral, you could take the standard part (though of course this will only work when the integral turns out to be a limited hyperreal).
