Release of HOL4 Kananaskis-7

I'm happy to announce the release of the latest version of HOL4 : Kananaskis-7.

Download it from http://hol.sourceforge.net.

Release notes follow.

Michael

--

                      Notes on HOL 4, Kananaskis-7 release

   We are pleased to announce the Kananaskis-7 release of HOL 4.

New features:

     * HolSmtLib supports Z3 proof reconstruction also for goals that
       involve fixed-width words, based on bit-blasting (cf. blastLib) and
       other word decision procedures.

     * HolSmtLib provides a translation from HOL into SMT-LIB 2 format.
       (Support for SMT-LIB 1.2 has been discontinued. Incompatibility.)

     * HolQbfLib supports checking both validity and invalidity
       certificates for Squolem 2.02. (Support for Squolem 1.x has been
       discontinued. Incompatibility.)

     * wordsSyntax.mk_word_replicate computes the width of the resulting
       word when applied to a numeral and a fixed-width word. Minor
       incompatibility.