HOL

Release Notes: HolSmtLib now also supports Z3 proof reconstruction for goals that involve fixed-width words and a translation from HOL into SMT-LIB 2 format. HolQbfLib supports checking for both validity and invalidity of certificates for Squolem 2.02. wordsSyntax.mk_word_replicate computes the width of the resulting word when applied to a numeral and a fixed-width word. The system supports syntax for decimal fractions. This syntax maps to division terms of the form n / 10m. In the core system, this syntax is enabled for the real, rational, and complex theories.

Release Notes: The HolSmtLib library now supports proof reconstruction for the SMT solver Z3. Many type variables can now be parsed and printed as lower-case Greek letters. Bounded rewrites work better. Simplification of terms involving the EL operator is better. Improved support for bag operations. Syntax updates for things like the universal set. Other minor enhancements and bugfixes.

Release Notes: There is now a Poly/ML implementation of HOL4 available for users on platforms other than Windows. Overloading can now target "syntactic patterns". The :string type is now an alias for :char list. Types can now be numerals. The finite cartesian product "array" type can now be written with square brackets. wordsLib now supports evaluation over non-standard word-sizes. Support for Unicode was added. Support for Patricia trees was added. Many other enhancements and bugfixes were made.

Release Notes: New set comprehension notation was added. SML string notation was added. Support for the XEmacs editor was added. Case expressions may now include literals as patterns. Inductive definitions are now made with respect to a varying monoset. Types that use abbreviated patterns are printed in abbreviated form. Support for rational numbers and fixed-length integers was added. Bugs that prevented some components from compiling under GCC 4 were fixed. Normalization in natural numbers and integers was fixed. Handling of empty strings was fixed.

Release Notes: This release adds theories of co-inductive (possibly infinite) labelled transition paths in pathTheory, and of sorting and list permutations in sortingTheory. It adds a new first-order proof tactic (called METIS_TAC) that uses an ordered resolution and paramodulation, and a 'boolification' tool that automatically defines functions that map data types to boolean vectors. Many extensions, bugfixes, and backwards incompatibilities.