On Monday, August 6, 2018, 9:12:36 AM GMT+2, Askar Safin <address@hidden> wrote:
This is not my library, it is Slawomir's one. I simply found it in the internet one day. I tried to CC him.
Askar Safin
>Воскресенье, 5 августа 2018, 14:49 +03:00 от Lawrence Paulson <
address@hidden>:
>
>That’s amazing! And it needs to be publicised more. Have you ever announced it to the Isabelle mailing list?
>Larry
>
>>
>>> Isabelle/ZF is untyped, which unfortunately means it can't use Isabelle's linear arithmetic decision procedures, so arithmetic reasoning is difficult. We don't have a construction of the rational numbers, let alone the complex numbers
>>
>> ==
>> Askar Safin