Theorem Proving in Higher Order Logics (Springer)