23 Feb
2016
23 Feb
'16
7:05 p.m.
On Mon, 22 Feb 2016, David Matthews wrote:
There is a configure option --enable-intinf-as-int. This causes polyimport to build the basis library with int as arbitrary precision integer rather than fixed precision.
I have adapted to this change here: http://isabelle.in.tum.de/repos/isabelle/rev/ad3eb2889f9a
It works fine. I am rather glad that only some ML pretty printing required a different (approximative) int type.
Makarius