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

Florian Haftmann florian.haftmann at informatik.tu-muenchen.de
Mon Dec 23 16:27:39 CET 2013

See now



On 12.12.2013 16:21, Florian Haftmann wrote:
>>> * 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
> _______________________________________________
> isabelle-dev mailing list
> isabelle-dev at in.tum.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev


PGP available:

-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 263 bytes
Desc: OpenPGP digital signature
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20131223/0f76eae7/attachment.sig>

More information about the isabelle-dev mailing list