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