[isabelle] RC5: Syntactic class bit_operations is gone
In 2020, there used to be a purely syntactic class for bitwise
This class is gone in RC5, and the closest match seems to be the class
semiring_bit_operations in Library/Bit_Operations.thy, but this has
This new class binds the infix syntax for (AND), (OR), (XOR) to these
I thought it would be standard to define syntactic type classes for
infix syntax first, and then add the axioms.
In my application, I cannot use the semiring_bit_operations class, as I
cannot define a mask function. However, I'd like to use the convenient
syntax, which is now somewhat blocked.
On Mon, 2021-02-08 at 22:42 +0100, Makarius wrote:
> Dear Isabelle users,
> the end of the Isabelle2021 release process is getting pretty close.
> Presumably the last release candidate is
> See again
> and 4 for further details.
> Any feedback about release candidates should be posted with a
> Subject including the version (not just a clone of this
> People who have tested earlier release candidates should definitely
> this one, otherwise some last-minute problems might remain
This archive was generated by a fusion of
Pipermail (Mailman edition) and