On Thu, 13 Oct 2011, Thomas Sewell wrote:
3) After adding a 400-element record to a test theory built on the HOL image.
Your original motivation was to isolate mysterious performance issues in
the record package. Did you now manage to pin that down in the
measurement?
In that case a bisection could reveal the point in history where the
change happened, so one might learn from it another detail about the ML
runtime-system.
Makarius
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
