A strong axiom of infinity for HOL
(for noframe browsers)