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.

What's New in This Release:
· 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.