src/Provers/clasimp.ML
2006-01-19 ago setup: theory -> theory;
2006-01-14 ago generic attributes;
2006-01-10 ago generic attributes;
2005-12-31 ago removed obsolete Provers/make_elim.ML;
2005-12-21 ago modified suffix for [iff] attribute
2005-10-17 ago functor: no Simplifier argument;
2005-08-16 ago classical rules must have names for ATP integration
2005-05-22 ago Simplifier already setup in Pure;
2005-03-03 ago Move towards standard functions.
2005-02-13 ago Deleted Library.option type.
2004-07-11 ago local_cla/simpset_of;
2004-06-21 ago Merged in license change from Isabelle2004
2002-09-30 ago Introduced addss', which adds asm_lr_simp_tac as a wrapper to the claset.
2002-03-05 ago iff: conditional rules declared as ``unsafe'';
2001-12-05 ago iff?: refer to Pure/ContextRules;
2001-10-23 ago iff: always rotate prems;
2001-08-09 ago corrected semantics of [iff] concerning rules with premises
2001-08-06 ago removed the warning from [iff]
2001-05-31 ago streamlined addIffs/delIffs, added warnings
2001-02-23 ago renamed addaltern to addafter, addSaltern to addSafter
2001-01-07 ago CHANGED_PROP;
2000-10-24 ago added clasimpset: unit -> clasimpset;
2000-09-20 ago made SML/NJ happy;
2000-09-19 ago added iff_add_global', iff_add_local' (syntax "iff?");
2000-09-13 ago Args.addN, Args.delN;
2000-09-07 ago tuned msg;
2000-09-05 ago added 'iff' declarations;
2000-09-02 ago added "slowsimp", "bestsimp";
2000-09-01 ago auto method: opt args;
2000-08-14 ago added "fastsimp";
2000-08-03 ago export get_local_clasimpset, clasimp_modifiers;
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