src/HOL/Induct/LList.ML
1998-08-06 paulson 1998-08-06 even more tidying of Goal commands
1998-07-24 berghofe 1998-07-24 Adapted to new datatype package.
1998-07-15 paulson 1998-07-15 More tidying and removal of "\!\!... from Goal commands
1998-07-15 paulson 1998-07-15 Removal of leading "\!\!..." from most Goal commands
1998-06-30 berghofe 1998-06-30 Adapted to new inductive definition package.
1998-06-26 paulson 1998-06-26 New rewrite unit_abs_eta_conv to compensate for unit_eq_proc
1998-06-25 wenzelm 1998-06-25 delsimprocs [unit_eq_proc];
1998-06-22 wenzelm 1998-06-22 isatool fixgoal;
1998-04-27 nipkow 1998-04-27 Renamed expand_const -> split_const.
1998-04-21 oheimb 1998-04-21 split_all_tac is now added to claset() _before_ other safe tactics
1998-01-08 paulson 1998-01-08 Tidied by adding more default simprules
1997-12-24 paulson 1997-12-24 New Auto_tac (by Oheimb), and new syntax (without parens), and expandshort
1997-11-05 paulson 1997-11-05 Adapted to removal of UN1_I, etc
1997-11-03 wenzelm 1997-11-03 isatool fixclasimp;
1997-10-17 nipkow 1997-10-17 setloop split_tac -> addsplits
1997-10-10 wenzelm 1997-10-10 fixed dots;
1997-06-06 paulson 1997-06-06 Removed a few redundant additions of simprules or classical rules
1997-05-07 paulson 1997-05-07 New directory to contain examples of (co)inductive definitions