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