From: Freek Verbeek <email@example.com>
I am trying to update some of my Isabelle 2020 theories to Isabelle 2021. I previously made use of the libraries "HOL-Word.Word” and "HOL-Word.Word_Bitwise” and see that these have been replaced with improved versions. I am now including "HOL-Library.Word”, but I cannot find some of the things previously available (or new versions of them). For example, I cannot find the signed shiftr operator >>>, functions such as to_bl and msb, or bitwise theorems such as to_bl_plus_carry.
Does anyone know where these can be found in Isabelle 2021? I am especially looking for the bitwise theorems over arithmetic, i.e., theorems similar to “twos_complement" and “to_bl_plus_carry".
From: Peter Lammich <firstname.lastname@example.org>
there is a "Word_Lib.Word_Lib_Sumo" theory, that includes everything
From: Florian Haftmann <email@example.com>
the NEWS file contains a lot of hints and detail concerning words.
The most important one is the last:
The »Word_Lib.Word_Lib_Sumo« is a practical starting point for
migrating, personally I recommend to get along without it and switch to
more selective imports.
Hope this helps,
Last updated: Jan 25 2022 at 02:35 UTC