On 05.02.19 13:18, Salomon Sickert wrote:
It should be easy to make this part of the formal session, with some
options [condition = ISABELLE_MLTON].
The 'export_code' command will have to emit generated files
(Generated_Files.add_files) to make the assembly work in Isabelle/ML.
I have
On 05.02.19 11:43, Peter Lammich wrote:
I just updated my Isabelle devel version (now on d21789843f01), and
immediately noticed that the displayed fonts are significantly blurry.
Find attached a side-by-side comparison of Isabelle-d21789843f01 (left)
and Isabelle-2018 (right). At least on my
On 05.02.19 20:19, Makarius wrote:
From a distance, I would say that this is a matter of the Java 11
font-renderer, which is provided by https://adoptopenjdk.net. The one by
Oracle is much worse -- OpenJdk not the non-free Java. (Note that the
license change of non-free Oracle Java no longer
Hello,
If I'm not mistaken, the default code setup for the "power" operation in
HOL is linear in the exponent (it just does multiplication n times). I
didn't find anything on faster exponentiation in the distribution or the
AFP. so in 154cf64e403e, I committed some material about exponentiation
Dear Manuel,
in the AFP there is Subresultants/Binary_Exponentiation.thy. Perhaps your
changes make this theory obsolete.
The Binary_Exponentiation algorithm is then later on used in
Berlekamp-Zassenhaus in modular arithmetic to compute inverses in prime-fields.
Cheers,
René
> Am 05.02.2019
>> To add a couple more to the list:
>>
>> — LTL has includes a parser that is used in an example and built using
>> LTL/examples/build_poly.sh
>>
>> — LTL_to_DRA can generate a tool using either LTL_to_DRA/Code/build_poly.sh
>> and LTL_to_DRA/Code/build_mlton.sh
>
> It should be easy to
