HOL Light Tools

This is a library of tools, tactics, and theories I have developed in HOL Light.

Some of these, such as the finite map theory, have been ported from the work of others, particularly in HOL4.

Notable things included:

• A port of the finite map theory from HOL4.
• A set of tools to enable proofs in an arbitrarily extended proof state.
• A small library about substitution.
• Additional definitions and lemmas for lists, sets, multisets, etc.
• Additional functions to manipulate terms and variables.
• A small library that statically counts the number of steps in an interactive proof.