src/Provers/hypsubst.ML
1996-11-01 paulson 1996-11-01 Replaced min by Int.min
1995-04-06 lcp 1995-04-06 Recoded with help from Toby to use rewriting instead of the subst rule -- the latter was too slow. But it must resort to the subst rule if the equality contains Vars.
1994-11-11 lcp 1994-11-11 Provers/hypsubst/REPEATN: deleted; using REPEAT_DETERM_N instead.
1994-11-02 lcp 1994-11-02 Provers/hypsubst: greatly simplified! No longer simulates a "eres_inst_tac" using rev_cut_eq; instead simply rotates the chosen equality to the end!
1994-10-19 lcp 1994-10-19 new comments explaining abandoned change
1994-01-18 lcp 1994-01-18 Updated refs to old Sign functions
1993-09-16 clasohm 1993-09-16 Initial revision