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.

Larry

_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Reply via email to