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-10-17 ago change_claset/simpset;
2003-08-20 ago new case_tac method
2002-03-06 ago tuned;
2001-10-14 ago eliminated atomize rules;
2001-01-16 ago tuned atomize;
2000-11-10 ago val atomize = thms "atomize'";
2000-11-03 ago "atomize" for classical tactics;
2000-09-05 ago tuned;
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 IFOL/FOL theories and packages;
1999-08-02 ago fixed Blast_Data;
1998-11-18 ago blast: cla_method';
1998-02-25 ago renamed rep_claset to rep_cs
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-03 ago adapted to new implicit claset;
1997-10-10 ago fixed dots;
1997-08-06 ago Moved functions from file "thy_data.ML".
1997-04-02 ago Now builds blast_tac
1997-03-27 ago Now uses the alternative (safe!) rules for ex1
1997-01-03 ago Implicit simpsets and clasets for FOL and ZF