src/HOL/Induct/LList.ML
2000-10-12 nipkow 2000-10-12 *** empty log message ***
2000-10-11 nipkow 2000-10-11 *** empty log message ***
2000-09-06 nipkow 2000-09-06 less_induct -> nat_less_induct
2000-08-30 nipkow 2000-08-30 introduced induct_thm_tac
2000-04-13 nipkow 2000-04-13 Times -> <*> ** -> <*lex*>
2000-03-13 wenzelm 2000-03-13 case_tac now subsumes both boolean and datatype cases;
2000-03-13 nipkow 2000-03-13 exhaust_tac -> cases_tac
2000-01-07 paulson 2000-01-07 tidied parentheses
1999-10-11 paulson 1999-10-11 replaced {x. True} by UNIV to work with the new simprule, Collect_const
1999-08-18 berghofe 1999-08-18 Eliminated some infixes.
1998-11-30 paulson 1998-11-30 Renamed subset_Sigma_llist to subset_Times_llist
1998-11-26 paulson 1998-11-26 tidied up list definitions, using type 'a option instead of unit + 'a, also using real typedefs instead of faking them with extra rules
1998-11-02 paulson 1998-11-02 Domain r, Range r replace fst``r, snd``r
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