2001-11-19 ago tuned;
2001-11-16 ago actually store "coinduct" rule;
2001-11-14 ago case_names;
2001-11-14 ago adapted primrec/datatype to Isar;
2001-11-13 ago rearranged inductive package for Isar;
2001-11-09 ago support co/inductive definitions in new-style theories;
2001-10-04 ago qualify MetaSimplifier;
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.;
1999-10-04 ago mk_frees, assume_read moved here;
1999-09-21 ago Mod because of new solver interface.
1999-02-03 ago standard spelling: type-checking
1999-01-19 ago removal of the (thm list) argument of mk_cases
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