[isabelle] RC5: Syntactic class bit_operations is gone



Hi List.

In 2020, there used to be a purely syntactic class for bitwise
operations: 

HOL/Word/Bits.bit_operations

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
axioms.

This new class binds the infix syntax for (AND), (OR), (XOR) to these
axioms.

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.

--
  Peter




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
> https://isabelle.sketis.net/website-Isabelle2021-RC5
> 
> See again
> https://isabelle-dev.sketis.net/phame/post/view/28/release_candidates_for_isabelle2021
> and 4 for further details.
> 
> 
> Any feedback about release candidates should be posted with a
> meaningful
> Subject including the version (not just a clone of this
> announcement).
> 
> People who have tested earlier release candidates should definitely
> follow
> this one, otherwise some last-minute problems might remain
> undetected.
> 
> 
> 	Makarius
> 





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