src/Provers/simplifier.ML
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.
1998-03-10 ago New simplifier flag for mutual simplification.
1998-03-06 ago Added delspilts, Addsplits, Delsplits.
1998-03-04 ago Reorganized simplifier. May now reorient rules.
1998-02-28 ago Little reorganization. Loop tactics have names now.
1998-02-09 ago Used THEN_ALL_NEW.
1997-12-04 ago added print_simpset;
1997-11-26 ago removed conv_prover;
1997-11-21 ago changed Pure/Sequence interface -- isatool fixseq;
1997-11-20 ago adapted print methods;
1997-11-04 ago type object = exn (enhance readability);
1997-11-03 ago new implicit simpset mechanism based on Sign.sg anytype data;
1997-09-29 ago Default simpset tactics now dereference "simpset"
1997-07-25 ago added prems argument to simplification procedures;
1997-07-23 ago added simplification meta rules;
1997-07-22 ago added print_ss;
1997-07-22 ago Removal of the tactical STATE
1997-07-16 ago fixed merge of internal simprocs;
1997-02-17 ago mk_rews: automatically includes strip_shyps, zero_var_indexes;
1997-02-15 ago added deleqcongs, richer rep_ss
1997-01-31 ago added addloop (and also documentation of addsolver
1997-01-17 ago addsimps, addeqcongs: replaced @ by gen_union;
1997-01-16 ago added termless parameter;
1997-01-10 ago cleaned up (real changes next time);
1996-05-29 ago Added addsolver
1996-04-23 ago *** empty log message ***
1996-02-16 ago Elimination of fully-functorial style.
1995-10-04 ago renamed SS to Simpset; fixed bug in merge_ss
1995-09-01 ago added global simpset
1995-03-30 ago Precedence of infixes is now 4 (just above that of :=)
1994-06-21 ago improved error msg
1994-05-31 ago simpset is hidden in a functor now.
1994-01-05 ago got rid of METAHYPS due to the change of the basic simplification routines
1993-11-25 ago asm_full_simp_tac now fails if there are no subgoals
1993-10-29 ago added infix delsimps
1993-10-01 ago asm_full_simp_tac now fails when applied to a state w/o subgoals.
1993-09-16 ago changed addcongs to addeqcongs in simplifier.ML
1993-09-16 ago Initial revision