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.


isabelle-dev mailing list

Reply via email to