[isabelle-dev] Word Libraries
florian.haftmann at informatik.tu-muenchen.de
Thu Aug 12 09:24:49 CEST 2021
> 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
> * 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.
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
> ▪ 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,
-------------- next part --------------
A non-text attachment was scrubbed...
Size: 228 bytes
Desc: OpenPGP digital signature
More information about the isabelle-dev