2001-11-19 ago tuned;
2001-11-16 ago additional P.marg_comment;
2001-11-14 ago use proper intr_names (for required case_names);
2001-11-14 ago adapted primrec/datatype to Isar;
2001-11-09 ago adapted to add_inductive_x;
2000-07-13 ago adapted PureThy.add_defs_i;
2000-05-05 ago use Sign.simple_read_term;
2000-03-13 ago adapted to new PureThy.add_thms etc.;
2000-01-13 ago change in add_thmss to suppress warning
1999-10-04 ago tuned;
1999-01-27 ago automatic insertion of datatype intr rules into claset
1999-01-19 ago removal of the (thm list) argument of mk_cases
1999-01-13 ago datatype package improvements
1999-01-12 ago eliminated global/local names;
1999-01-12 ago eliminated tthm type and Attribute structure;
1999-01-07 ago ZF: the natural numbers as a datatype
1999-01-06 ago induct_tac and exhaust_tac
1998-12-28 ago revised datatype definition package