src/HOL/datatype.ML
1996-03-13 ago modified primrec so it can be used in MiniML/Type.thy
1996-01-30 ago expanded tabs
1996-01-29 ago changed the way simpsets and information about datatypes are stored
1995-11-21 ago added call of store_datatype
1995-10-11 ago All constants introduced by datatype now operate on class term explicitly.
1995-03-30 ago removed unnecessary parentheses from the generated rules
1995-03-17 ago fixed two severe bugs in calc_xrules and case_rule
1995-03-03 ago new version of HOL with curried function application