Include documentation on ADT in the manual, from Andrea's thesis and the paper Mechanized HOL Reasoning in Set Theory.