Dr Petros Papapanagiotou

Senior Scala Engineer

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: