Let’s be clear: the semantics of type int is well-defined. It denotes the set 
of integers over a specific finite range of values, and if this range is 
exceeded, exception Overflow is raised. If one’s requirements fit within that 
range of values then there is no rational reason to suffer a penalty in order 
to widen that range.


> On 3 Nov 2016, at 13:46, Makarius <makar...@sketis.net> wrote:
> Luckily the situation is not as bad, and David Matthews continues to
> consolidate the new compiler and run-time system: Isabelle is already a
> bit faster than before, while still remaining true to mathematical
> semantics of int.

isabelle-dev mailing list

Reply via email to