Mark D. Aagaard, John Harrison: Theorem Proving in Higher Order Logics, 13th International Conference, TPHOLs 2000, Portland, Oregon, USA, August 14-18, 2000, Proceedings. Lecture Notes in Computer Science 1869, Springer 2000, ISBN 3-540-67863-8