Thanks for those figures. They just emphasize how limited benchmarking is. For running Isabelle, Poly/ML is consistently 50% faster than SML/NJ. It makes virtually no use of floating point, though. -- Larry Paulson