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
