hol-1.4: Higher order logic