Dear Brian,
> 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.
The issue with code generation is
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 modification
Certainly an interesting idea. HOL4 also uses separate constants.
Thanks for trying this out!
I don't know who is going to fix code generation though...
Larry
On 12 Feb 2008, at 02:21, Brian Huffman wrote:
> Hello all,
>
> Recently I tested a variation of HOL/ex/Binary.thy: Instead of using
Hello all,
Recently I tested a variation of HOL/ex/Binary.thy: Instead of using a
function "bit :: nat => bool => nat", I replaced this with a pair of
functions, "bit0 :: nat => nat" and "bit1 :: nat => nat" which are
equal to "bit False" and "bit True", respectively. (The modified
theory
