HOL 4

HOL short from Higher Order Logic is a programming environment in which theorems can be proved and proof tools implemented.
Built-in decision procedures and theorem provers can automatically establish many simple theorems. An oracle mechanism gives access to external programs such as SAT and BDD engines.
HOL 4 is particularly suitable as a platform for implementing combinations of deduction, execution and property checking.
Enhancements:
- 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.