S. Agerholm, “LCF Examples in HOL”, BRICS, vol. 1, no. 18, Jun. 1994.