STEP HOL Utilities This repository contains general utility functions and tactics written in Standard ML, for use in the HOL4 theorem prover. The code is available under the MIT license.