All releases tagged Major feature enhancements
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.
