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