HOL(y) Hammer

Learning-assisted automated reasoning for HOL Light

HH logo
universitat innsbruck
radboud univeristeit nijmegen

Request Advice:

Input the HOL Light formula to prove and select HOL Light session:

Upload Own Development:

Choose either a single HOL Light ".ml" file, or a ".tgz" file with a "make.ml" in top directory:
  • File:
  • Session name:
  • Password:
  • Upload against:

Uploaded Developments


Download (Local Install)

  • Download source code: version 0.13.
  • Unpack in your HOL Light directory and follow the instructions in the included README file.

Back to top