src/HOL/Lex/MaxChop.ML
2004-02-19 paulson 2004-02-19 removal of the legacy ML structure List
2000-10-25 wenzelm 2000-10-25 use Library/List_Prefix;
2000-09-07 wenzelm 2000-09-07 chop_nonempty: accomodate new qed_spec_mp;
2000-08-30 nipkow 2000-08-30 introduced induct_thm_tac
2000-03-30 nipkow 2000-03-30 recdef.rules -> recdef.simps
1999-07-08 paulson 1999-07-08 Now if_weak_cong is a standard congruence rule
1999-04-29 nipkow 1999-04-29 Proof mods due to eta contraction during rewriting.
1998-07-24 berghofe 1998-07-24 Adapted to new datatype package.
1998-07-21 wenzelm 1998-07-21 isatool expandshort;
1998-07-18 nipkow 1998-07-18 Simplified last proof.
1998-07-12 wenzelm 1998-07-12 isatool expandshort;
1998-07-03 nipkow 1998-07-03 Removed leading !! in goals.
1998-06-22 wenzelm 1998-06-22 isatool fixgoal;
1998-05-11 nipkow 1998-05-11 Reordered a few parameters.
1998-04-27 nipkow 1998-04-27 Added conversion of reg.expr. to automata. Renamed expand_const -> split_const.
1998-03-10 nipkow 1998-03-10 New scanner in abstract form.