Stefan Berghofer, Markus Wenzel. Inductive Datatypes in HOL - Lessons Learned in Formal-Logic Engineering. In Yves Bertot, Gilles Dowek, André Hirschowitz, C. Paulin, Laurent Théry, editors, Theorem Proving in Higher Order Logics, 12th International Conference, TPHOLs 99, Nice, France, September, 1999, Proceedings. Volume 1690 of Lecture Notes in Computer Science, pages 19-36, Springer, 1999. [doi]
Abstract is missing.