2000-07-25 ago added clarsimp method;
2000-07-21 ago strengthened force_tac by using new first_best_tac
2000-03-31 ago added change_global/local_css;
2000-03-15 ago include Splitter.split_modifiers;
2000-01-28 ago HEADGOAL;
2000-01-28 ago replaced FIRSTGOAL by FINDGOAL (backtracking!);
1999-10-27 ago clarsimp_tac now copes with the (unwanted) case that the simplifier splits
1999-09-21 ago setup for refined facts handling;
1999-09-02 ago renamed improper method 'clarsimp' to 'clarsimp_tac';
1999-09-01 ago Method.insert_tac;
1999-08-30 ago auto: CHANGED;
1999-08-18 ago Method.modifier;
1999-08-02 ago tuned;
1999-07-30 ago eliminated METHOD0 in favour of same_tac;
1998-11-29 ago method brute_force = ALLGOALS force_tac;
1998-11-18 ago method setup;
1998-10-23 ago corrected auto_tac (applications of unsafe wrappers)
1998-09-25 ago deleted illegal "op"
1998-09-24 ago removed addcongs2 and delcongs2
1998-09-21 ago improved addbefore and addSbefore
1998-09-11 ago added clarsimp_tac and Clarsimp_tac
1998-07-30 ago functorized Clasimp module;
1998-05-02 ago added CLASIMPSET(') tacticals;
1998-05-01 ago Auto_tac: now uses enhanced version of asm_full_simp_tac,
1998-03-10 ago renamed smart_tac to force_tac, slight improvement of force_tac
1998-02-26 ago added smart_tac
1998-02-25 ago factored out common code of HOL/simpdata.ML and FOL/simpdata.ML concerning