src/ZF/Tools/inductive_package.ML
1999-01-12 ago eliminated global/local names;
1999-01-12 ago eliminated tthm type and Attribute structure;
1998-12-28 ago revised inductive definition package