Install hol-light by entering the following commands in the terminal:
sudo apt update sudo apt install hol-light
Description:
HOL Light theorem prover
HOL Light is an interactive theorem prover for Higher-Order Logic with a very simple logical core running in an OCaml toplevel. HOL Light is famous for the verification of floating-point arithmetic as well as for the Flyspeck project, which aims at the formalization of Tom Hales' proof of the Kepler conjecture.
Homepage: http://www.cl.cam.ac.uk/~jrh13/hol-light/
Version: 20170706-0ubuntu4
Section: universe/math