On 07/11/2017 23:13, Makarius wrote:
For Flyspeck-Tame a small performance loss remains. It might be worth trying to configure the Isabelle/HOL codegen to use FixedInt instead of regular (unbounded) Int. Thus it could become faster with Poly/ML 5.7.1 than with 5.6.
Just as for Isabelle itself, I don't want generated code to abort with overflow or even worse to overflow silently.
Tobias
smime.p7s
Description: S/MIME Cryptographic Signature
_______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
