[isabelle-dev] binary arithmetic optimization

Gerwin Klein gerwin.klein at nicta.com.au
Tue Feb 12 21:56:15 CET 2008


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




More information about the isabelle-dev mailing list