2006-01-19 ago setup: theory -> theory;
2005-12-31 ago removed obsolete Provers/make_elim.ML;
2005-12-30 ago provide cla_dist_concl;
2005-12-08 ago swap: no longer pervasive;
2005-12-08 ago Classical.swap;
2005-12-06 ago removed thms 'swap' and 'nth_map' from ML toplevel
2005-10-17 ago change_claset/simpset;
2005-03-03 ago Move towards standard functions.
2001-12-04 ago hyp_subst_tac';
2001-10-14 ago improved atomize setup;
2001-07-25 ago partial restructuring to reduce dependence on Axiom of Choice
2001-07-22 ago the_equality [intro];
2001-01-16 ago tuned atomize;
2000-11-10 ago val atomize = thms "atomize'";
2000-11-03 ago "atomize" for classical tactics;
2000-10-17 ago renaming of contrapos rules
2000-10-12 ago renamed ?Pa to ?Q in swap
2000-09-15 ago renamed (most of...) the select rules
2000-09-05 ago tuned;
2000-08-04 ago val rev_eq_reflection = def_imp_eq;
2000-07-30 ago updated ObtainFun;
2000-06-28 ago declaring and using cla_make_elim
2000-01-05 ago ObtainFun;
1999-08-25 ago proper bootstrap of HOL theory and packages;
1999-08-02 ago tuned;
1999-07-15 ago qed_goal -> Goal
1998-11-18 ago blast: cla_method';
1998-02-25 ago renamed rep_claset to rep_cs
1998-01-08 ago added select_equality to the implicit claset
1997-12-23 ago Better equality handling in Blast_tac, usingd a new variant of hyp_subst_tac
1997-11-26 ago The change from iffE to iffCE means fewer case splits in most cases. Very few
1997-11-20 ago Renamed "overload" to "overloaded" for sml/nj compatibility
1997-11-12 ago added thin_refl to hyp_subst_tac
1997-11-12 ago restored last version
1997-11-12 ago simpdata.ML: renamed split_prem_tac to split_asm_tac, added split_if_asm
1997-11-06 ago hyp_subst_tac checks if the equality has type variables and uses a suitable
1997-11-03 ago adapted to new implicit claset;
1997-11-01 ago New Blast_tac (and minor tidying...)
1997-10-10 ago fixed dots;
1997-08-06 ago Moved some functions which used to be part of thy_data.ML
1997-04-21 ago New elimination rule for "unique existence"
1997-04-03 ago Declares overloading for if-and-only-if
1997-04-02 ago Installation of blast_tac
1996-09-12 ago Tidied many proofs, using AddIffs to let equivalences take