Hi Gerwin, > This sounds good, but I don't quite remember any more what exactly that was, > can you give a summary? > > As you know, it's a bit of work to check that for l4v, esp since it is still > on Isabelle2020 (no real issues, mostly organisational upheavals have taken > up all available attention). It will take a while, but it looks like it will > break in the usually hopefully small ways. > > Do you have a list of changes that users will likely ned to apply?
it’s in the NEWS
> * Infix syntax for bit operations AND, OR, XOR is now organized in
> bundle bit_operations_syntax. INCOMPATIBILITY.
>
> * Bit operations set_bit, unset_bit and flip_bit are now class
> operations. INCOMPATIBILITY.
>
> * Theory Bit_Operations is now part of HOL-Main. Minor INCOMPATIBILITY.
>
> * Simplified class hierarchy for bit operations: bit operations reside
> in classes (semi)ring_bit_operations, class semiring_bit_shifts is
> gone.
>
> * Abbreviation "max_word" has been moved to session Word_Lib in the AFP,
> as also have constants "shiftl1", "shiftr1", "sshiftr1", "bshiftr1",
> "setBit", "clearBit". See there further the changelog in theory Guide.
> INCOMPATIBILITY.
and as a separate section in the »Guide« in session Word_Lib:
> ➧[Changes since AFP 2021] ~
>
> ▪ Theory \<^theory>‹Word_Lib.Ancient_Numeral› is no part of
> \<^theory>‹Word_Lib.Word_Lib_Sumo›
> any longer.
>
> ▪ Infix syntax for \<^term>‹(AND)›, \<^term>‹(OR)›, \<^term>‹(XOR)›
> organized in
> syntax bundle \<^bundle>‹bit_operations_syntax›.
>
> ▪ Abbreviation \<^abbrev>‹max_word› moved from distribution into theory
> \<^theory>‹Word_Lib.Legacy_Aliases›.
>
> ▪ Operation \<^const>‹test_bit› replaced by input abbreviation
> \<^abbrev>‹test_bit›.
>
> ▪ Operation \<^const>‹shiftl› replaced by abbreviation \<^abbrev>‹shiftl›.
>
> ▪ Operation \<^const>‹shiftr› replaced by abbreviation \<^abbrev>‹shiftr›.
>
> ▪ Operation \<^const>‹sshiftr› replaced by abbreviation
> \<^abbrev>‹sshiftr›.
>
> ▪ Abbreviations \<^abbrev>‹bin_nth›, \<^abbrev>‹bin_last›,
> \<^abbrev>‹bin_rest›,
> \<^abbrev>‹bintrunc›, \<^abbrev>‹sbintrunc›, \<^abbrev>‹norm_sint›,
> \<^abbrev>‹bin_cat› moved into theory
> \<^theory>‹Word_Lib.Legacy_Aliases›.
>
> ▪ Operations \<^abbrev>‹shiftl1›, \<^abbrev>‹shiftr1›,
> \<^abbrev>‹sshiftr1›, \<^abbrev>‹bshiftr1›,
> \<^abbrev>‹setBit›, \<^abbrev>‹clearBit› moved from distribution into
> theory
> \<^theory>‹Word_Lib.Legacy_Aliases› and replaced by input abbreviations.
>
> ▪ Operation \<^const>‹complement› replaced by input abbreviation
> \<^abbrev>‹complement›.
Hope this helps,
Florian
OpenPGP_signature
Description: OpenPGP digital signature
_______________________________________________ isabelle-dev mailing list [email protected] https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev
