[isabelle-dev] NEWS: HOL-Word
Gerwin Klein
gerwin.klein at nicta.com.au
Mon Aug 20 04:41:46 CEST 2007
* HOL-Word:
New extensive library and type for generic, fixed size machine
words, with arithmetic, bit-wise, shifting and rotating operations,
reflection into int, nat, and bool lists, automation for linear
arithmetic (by automatic reflection into nat or int), including
lemmas on overflow and monotonicity. Instantiated to all appropriate
arithmetic type classes, supporting automatic simplification of
numerals on all operations. Jointly developed by NICTA, Galois, and
PSU.
* Library/Boolean_Algebra: locales for abstract boolean algebras.
* Library/Numeral_Type: numbers as types, e.g. TYPE(32).
This is the initial check-in of the word library. There are still some small
todo items open, mainly adding a README.html/document and moving some of the
generic lemmas to their appropriate place in distribution.
Cheers,
Gerwin
More information about the isabelle-dev
mailing list