1997-04-03 nipkow 1997-04-03 Removed (Unit) in Prod. Added test for ancestor Nat in datatype.
1996-11-28 paulson 1996-11-28 Replaced map...~~ by
1996-09-26 paulson 1996-09-26 Ran expandshort
1996-08-02 berghofe 1996-08-02 Replaced prove_case_cong by Konrad Slinds optimized version.
1996-06-18 paulson 1996-06-18 Translation infixes <->, etc., no longer available at top-level
1996-04-26 clasohm 1996-04-26 added changes by Konrad to prove_nchotomy
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