src/Provers/simplifier.ML
2001-11-28 ago theory data: removed obsolete finish method;
2001-11-24 ago generic_merge;
2001-11-08 ago theory data: finish method;
2001-10-25 ago 'simplified' att: args;
2001-10-04 ago qualify MetaSimplifier;
2001-01-07 ago CHANGED_PROP;
2000-11-07 ago Moved meta simplification stuff from Thm to MetaSimplifier.
2000-09-19 ago tuned args;
2000-09-15 ago safe_asm_full_simp_tac is back (for compat);
2000-09-13 ago Args.addN, Args.delN;
2000-09-07 ago tuned att names / msgs;
2000-09-05 ago removed 'other' modifier;
2000-08-29 ago made SML/XL happy;
2000-08-29 ago proper cong setup;
2000-08-03 ago unknown_theory/proof/context;
2000-07-25 ago tuned msg;
2000-07-21 ago removed safe_asm_full_simp_tac
2000-05-31 ago Toplevel.no_timing;
2000-05-17 ago export generic_simp_tac;
2000-05-05 ago use Args.colon / Args.parens;
2000-04-17 ago Pretty.chunks;
2000-04-13 ago added simp_options;
2000-04-04 ago print_simpset / print_claset command;
2000-03-31 ago use Attrib.add_del_args;
2000-03-15 ago export change_global_ss, change_local_ss;
2000-03-08 ago fixed section syntax;
2000-02-14 ago easy_setup: fixed mksimps;
2000-02-10 ago added easy_setup;
2000-01-29 ago simp_all method;
2000-01-28 ago HEADGOAL;
2000-01-28 ago replaced FIRSTGOAL by FINDGOAL (backtracking!);
1999-09-29 ago mk_simps: do *not* include Thm.strip_shyps o Drule.zero_var_indexes
1999-09-21 ago merged in lost update;
1999-09-21 ago Solvers are now named and stamped.
1999-09-21 ago setup for refined facts handling;
1999-09-01 ago Method.insert_tac;
1999-08-18 ago Method.modifier;
1999-08-16 ago forgot to write back adaption of onlysimps
1999-08-16 ago exchanged finish_tac and unsafe_finish_tac (the more important one) in simpset
1999-08-05 ago change_simpset_of;
1999-07-30 ago eliminated METHOD0 in favour of same_tac;
1999-07-13 ago same_tac;
1999-07-06 ago simp only: attribute, method arg;
1999-04-30 ago theory data: copy;
1999-04-27 ago improper simp methods;
1999-03-17 ago Theory.sign_of;
1999-01-12 ago eliminated tthm type and Attribute structure;
1998-11-18 ago export simp_modifiers;
1998-11-16 ago all modifiers turned into attributes;
1998-11-09 ago local simpset theory data;
1998-06-25 ago added XX_YY_rewrite: simpset -> cterm -> thm;
1998-06-10 ago Context.the_context;
1998-06-10 ago adapted to TheoryDataFun interface;
1998-06-05 ago accomodate tuned version of theory data;
1998-04-29 ago tuned setup;
1998-04-04 ago tuned comments;
1998-04-03 ago tuned names;
1998-03-12 ago addloop: added warning in case of overwriting a looper
1998-03-12 ago Used merge_alists for loopers.
1998-03-10 ago The new asm_lr_simp_tac is the old asm_full_simp_tac.