Email Gateway (Mar 05 2021 at 10:00): Email Gateway (Mar 05 2021 at 10:00):From: Freek Verbeek <freek@vt.edu>
Dear all,
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".
Best regards,
Freek
Email Gateway (Mar 05 2021 at 10:10):From: Peter Lammich <lammich@in.tum.de>
Hi Freek,
there is a "Word_Lib.Word_Lib_Sumo" theory, that includes everything
...
Email Gateway (Mar 05 2021 at 11:12):From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>
Hi Freek,
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,
Florian
OpenPGP_signature
Last updated: Jul 15 2022 at 23:21 UTC