Binary package “hol-light” in ubuntu eoan

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 aimed at the
 formalization of Tom Hales' proof of the Kepler conjecture.