src/Provers/hypsubst.ML
2001-12-05 ago 'symmetric' attribute moved to Pure/calculation.ML;
2001-11-21 ago use tracing function for trace output;
2001-01-07 ago CHANGED_PROP;
2000-09-07 ago tuned msg;
2000-08-28 ago Method.SIMPLE_METHOD';
2000-08-17 ago added 'symmetric' attribute;
2000-08-14 ago added hypsubst;
2000-08-04 ago added rev_eq_reflection;
1997-12-23 ago Better equality handling in Blast_tac, usingd a new variant of hyp_subst_tac
1997-11-26 ago updated comment
1997-11-12 ago added thin_refl to hyp_subst_tac
1997-11-06 ago hyp_subst_tac checks if the equality has type variables and uses a suitable
1997-07-22 ago Removal of the tactical STATE
1997-03-07 ago Prevent permutation of assumptions in hyp_subst_tac
1997-03-05 ago Now uses rotate_tac and eta_contract_atom for greater speed
1996-11-12 ago Removed a call to polymorphic mem
1996-11-01 ago Replaced min by Int.min
1995-04-06 ago Recoded with help from Toby to use rewriting instead of the
1994-11-11 ago Provers/hypsubst/REPEATN: deleted; using REPEAT_DETERM_N instead.
1994-11-02 ago Provers/hypsubst: greatly simplified! No longer simulates a
1994-10-19 ago new comments explaining abandoned change
1994-01-18 ago Updated refs to old Sign functions
1993-09-16 ago Initial revision