Welcome to HOLALA
HOLALA is HOL Light with an extended kernel. Instead of taking only = as primitive symbol, HOLALA takes also ∀ and ⇒ as primitive symbols.
Efficiency
It has been proved that simply by extending the kernel, the size of proof files got reduced to 64.36% (for OpenTheory standard library). Together with Holide (proof translator) and Dedukti (proof checker), we managed to improve the translation time by 41.81%. The corresponding Dedukti files got reduced to about 64.92% with a proof checking speed improvement of 38.04%.