[isabelle-dev] 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.

Concerning bit type vs. bit classes, I finally decicided to follow the
naming convention found in the abstract algebra theories of Main HOL,
i.e. »Bit« for theory with type bit and »Bits« for theory with bit type
classes.  See now

http://isabelle.in.tum.de/repos/isabelle/rev/3324a0078636

I have considered to rename type »bit« to »z2« but this inevitably would
raise further issues, e.g. renaming »nibble« to »z16« etc.

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