[isabelle-dev] Integers in Poly/ML

Lawrence Paulson lp15 at cam.ac.uk
Wed Nov 2 13:07:54 CET 2016

David Matthews is working on a new release of Poly/ML in which the default type of integers is fixed-precision. A configuration option can restore the former set up, but that might be a mistake: I modified MetiTarski to use large integers only where needed and saw runtime decrease by around 30%. We could do the same. I imagine that we need large integers almost nowhere. Now consider that every bound variable is represented internally by an integer.


More information about the isabelle-dev mailing list