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.