[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