The HolLight folder contains the skeleton of an instance of Logic.Logic for the logic of the HOL light theorem prover, see https://en.wikipedia.org/wiki/HOL_Light.