John Harrison: Binary Decision Diagrams as a HOL Derived Rule. Comput. J. 38(2): 162-170 (1995)