Hi,
indeed.
You can write simpler though: `real_integral (:real) f `.
Regards,
V.
--
Vincent Aravantinos
Analysis and Design of Dependable Systems
fortiss GmbH <www.fortiss.org/en>
Guerickestrasse 25 | 80805 Munich | Germany
----- Original Message -----
> 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
>
------------------------------------------------------------------------------
_______________________________________________
hol-info mailing list
[email protected]
https://lists.sourceforge.net/lists/listinfo/hol-info
