Michael Norrish

Right - I did experiment with full term sharing but I got quite poor results. It's possible I was doing something wrong, but my memory is that the tables were...

Building the core theories is a somewhat reasonable performance test. Theory build times are logged to `tools-poly/build-logs/` and you can compare times with the `developers/comparelogs` tool. You can also enable...

Thanks for the update!

Is there something we could merge on this front?

Any further word on this?

I'm happy to be advised by those more knowledgeable than I. For the moment, it sounds as if this still up in the air, but I'm happy with the prospect...

Good to hear! Thanks.

However, see also: http://isabelle.systems/zulip-archive/stream/247541-Mirror:-Isabelle-Users-Mailing-List/topic/.5Bisabelle.5D.20Wrong.20semantics.20for.20fmul_add.20in.20afp.2FIEEE_Float.2E.2E.2E.html which suggests that the behaviour exercising them was indeed the sign of the zeroes.

Seems like the expression in the quoted definition in the first post might need changing.

The new/fixed Isabelle code (from the development version of the AFP) has: ``` definition fmul_add :: "roundmode ⇒ ('t ,'w) float ⇒ ('t ,'w) float ⇒ ('t ,'w) float ⇒...