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

[Florian Haftmann]

See now

	http://isabelle.in.tum.de/repos/isabelle/rev/d6cf9a5b9be9

	Florian

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:
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://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20131223/0f76eae7/attachment.sig>