The HOL Light interactive theorem prover written by John Harrison is released to OPAM as a package. Its first new version available on OPAM is 3.0.
It now provides hol.sh which is a script that will launch an OCaml REPL that enables interactive theorem proving. Combined with a VSCode plugin for HOL Light, this gives a nice theorem proving experience…! For more details, please visit:
- The website: https://hol-light.github.io/
- The main repo: GitHub - jrh13/hol-light: The HOL Light theorem prover