Dear All,
I would like to know if the following definition in HOL Light
`real_integral {x:real| T} f `
is equivalent to int_{\-inf}^{\inf} f(x) dx.
Note: math formula written in latex.
Regards
------------------------------------------------------------------------------
_______________________________________________ hol-info mailing list [email protected] https://lists.sourceforge.net/lists/listinfo/hol-info
