[isabelle] bit vs. bool in HOL-Word

Hello all,
I have been revisiting the HOL-Word theories, and a central question
which has come to my mind is how bits are to be represented.  Some
theories are just using bool, but some use a dedicated but also
two-valued type bit.  This mixture is awkward.  Further, it seems to me
that the use of the bit type (in connection with the pseudo infix
constructor _ BIT _, which is the seed of almost all further usages of
type bit) goes back to the ancient numeral representation as signed bit
strings, which is now gone.
So, I would call for feedback from users of the HOL-Word theories:

* Is there a reason to prefer bit over bool or the other way round, and
if yes, in which situations?  Or does that just appear as accident?

* If bool would be the preferred type, is it feasible (wrt. to existing
applications »outside there«) to replace bit by bool entirely? This
could also include input syntax 0 and 1 for False and True respectively,
a conversion of_bool :: bool => 'a::zero_neq_one etc.

Suggestions welcome,


PGP available:

Attachment: signature.asc
Description: OpenPGP digital signature

This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.