[isabelle-dev] Word Libraries

[Florian Haftmann]

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

-------------- next part --------------
A non-text attachment was scrubbed...
Name: OpenPGP_signature
Type: application/pgp-signature
Size: 228 bytes
Desc: OpenPGP digital signature
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20210812/ca357645/attachment.sig>