The difference is substantial and uniform. I attach log files summarising MetiTarski’s performance by nearly 900 examples. You will note that total CPU time is way down, and problems consistently run much faster using fixedprecision arithmetic. Both runs involve the new version of Poly/ML, compiled with GMP. Note that MetiTarski makes heavy use of large integers, hundreds or thousands of digits long, because of its use of rational numbers. I actually can’t think of many places where Isabelle would need large integers, so it would probably benefit even more than MetiTarski does. Larry

STATUSMetit2016101160test3polyml.log
Description: Binary data
STATUSMetit2016103160fixedint.log
Description: Binary data
_______________________________________________ isabelledev mailing list isabelle...@in.tum.de https://mailmanbroy.informatik.tumuenchen.de/mailman/listinfo/isabelledevAdvertising