[isabelle-dev] [isabelle] bit vs. bool in HOL-Word

[Florian Haftmann]

>> * Concerning Bit.thy – this is something separate, a formalisation of
>> the Z2 field actually.  It stand aparat, and references of the Word
>> theories to bit should be replaced by bool.
>>
>> * Concerning bit operations – these should use bool uniformly.  Both
>> explicit list conversions and implicit structural operation like
>> test_bit and set_bit are relevant for user space. _ BIT _ is a historic
>> accident.  The idea is to clearly separate the bit operations into
>> separate HOL-Library theories, to make them properly available for
>> applications which do not need words but bits.
> 
> See now
> 
> http://isabelle.in.tum.de/~haftmann/cgi-bin/repos/bit_bool/
> http://isabelle.in.tum.de/~haftmann/cgi-bin/repos/bit_bool_afp/
> 
> where bool replaces bit as digit type throughout.
> 
> I invite users with heavy applications of the Word library to check this
> first before bringing it upstream.

Shall I assume that the silence on this thread means that everybody is
fine with pushing this matter?

If silence continues beyond Dec 21st, I will interpret this as »Go!«.
Otherwise just give me a shout.

	Florian


-- 

PGP available:
http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de

-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 263 bytes
Desc: OpenPGP digital signature
URL: <https://mailmanbroy.informatik.tu-muenchen.de/pipermail/isabelle-dev/attachments/20131212/b54b5d53/attachment.asc>