[isabelle-dev] binary arithmetic optimization

[Gerwin Klein]

On Tuesday 12 February 2008, Brian Huffman wrote:
> Today I modified a copy of Isabelle/HOL in this way; everything seems
> to work just fine, and binary arithmetic works faster. However, code
> generation will need a bit more work, and the HOL/Word library will
> need some non-trivial modifications.

Sounds good to me, as long as I don't have to be the one who does those 
non-trivial Word library modifications ;-)

Cheers,
Gerwin