An implementation of higher-order logic (HOL) in F#. Based on hol-light, Isabelle, and HOL4.