S. Agerholm, “LCF Examples in HOL”, BRICS, bd. 1, nr. 18, jun. 1994.