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
> [email protected]
> 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
signature.asc
Description: OpenPGP digital signature
_______________________________________________ isabelle-dev mailing list [email protected] https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
