Agerholm, S. LCF Examples in HOL. BRICS 1994, 1.