Reasoning with Inductively Defined Relations in the HOL Theorem Prover - Camilleri, J; Melham, T (Computer Laboratory‚ University of Cambridge, 1992)