2004-06-09 nipkow 2004-06-09 added a lemma lfp_ordinal_induct
2003-08-27 skalberg 2003-08-27 Converted to new style theories.
2000-10-12 nipkow 2000-10-12 induct -> lfp_induct
2000-10-11 nipkow 2000-10-11 *** empty log message ***
2000-09-23 paulson 2000-09-23 tidied, removing obsolete "goal" commands
2000-07-24 wenzelm 2000-07-24 avoid referencing thy value;
1998-08-13 paulson 1998-08-13 even more tidying of Goal commands
1998-06-30 berghofe 1998-06-30 Removed structure Prod_Syntax.
1997-10-10 wenzelm 1997-10-10 fixed dots;
1996-07-17 pusch 1996-07-17 removed superfluous Park-induct rule
1996-05-23 berghofe 1996-05-23 Replaced fast_tac by Fast_tac (which uses default claset) New rules are now also added to default claset.
1996-05-17 nipkow 1996-05-17 Moved split_rule et al from ind_syntax.ML to Prod.ML. Used split_rule in Lfp.ML and Trancl.ML.
1996-03-06 paulson 1996-03-06 Ran expandshort
1996-01-30 clasohm 1996-01-30 expanded tabs
1995-10-04 clasohm 1995-10-04 added local simpsets; removed IOA from 'make test'
1995-05-22 nipkow 1995-05-22 Added Park induction to Lfp. Added Lambda to Makefile.
1995-05-09 nipkow 1995-05-09 Prod is now a parent of Lfp. Added thm induct2 to Lfp. Changed the way patterns in abstractions are pretty printed. It has become simpler now but fails if split has more than one argument because then the ast-translation does not match.
1995-03-03 clasohm 1995-03-03 new version of HOL with curried function application