Recording and Refactoring HOL Light Tactic Proofs

Mark Adams, David Aspinall

Research output: Chapter in Book/Report/Conference proceedingConference contribution


In this article we present a mechanism for recording HOL Light tactic proofs in a hierarchical tree structure, with information stored at the level of atoms in the user’s ML proof script. This is written to support refactoring of tactic proofs, so that single-tactic packaged-up proofs can be flattened to a series of interactive tactic steps, and vice versa. It also provides a good basis for proof visualisation and for proof querying capability. The techniques presented can be adapted straightforwardly to other systems.
Original languageEnglish
Title of host publicationProceedings of the IJCAR workshop on Automated Theory Exploration
Number of pages6
Publication statusPublished - Jun 2012


Dive into the research topics of 'Recording and Refactoring HOL Light Tactic Proofs'. Together they form a unique fingerprint.

Cite this