Automating Recursive Type Definitions in Higher Order Logic - Melham, T (Computer Laboratory‚ University of Cambridge, 1988)