src/Provers/eqsubst.ML
2005-06-17 wenzelm 2005-06-17 added Id;
2005-05-19 dixon 2005-05-19 lucas - bugfix to subst in assumptions: fixed index error for conditional rules.
2005-05-18 dixon 2005-05-18 lucas - fixed subst in assumptions to count redexes from left to right.
2005-05-13 dixon 2005-05-13 lucas - fixed bug with uninstantiated type contexts in eqsubst and added the automatic removal of duplicate subgoals (when there are no flex-flex constraints)
2005-05-06 dixon 2005-05-06 lucas - added ability to provide multiple replacements for subst: syntax is now: subst (1 3) myrule
2005-05-05 dixon 2005-05-05 lucas - added option to select occurance to rewrite e.g. (occ 4)
2005-05-03 dixon 2005-05-03 lucas - improved interface to isand.ML and cleaned up clean-unification code, and added some better comments.
2005-04-26 dixon 2005-04-26 lucas - updated to reflect isand.ML update
2005-04-22 dixon 2005-04-22 lucas - fixed a big with renaming of bound variables. Other small changes.
2005-02-27 dixon 2005-02-27 lucas - added more comments and an extra type to clarify the code.
2005-02-19 dixon 2005-02-19 lucas - re-arranged code and added comments. Also added check to make sure the subgoal that we are being applied to exists. If it does not, empty seq is returned.
2005-02-02 paulson 2005-02-02 improved handling of chained facts
2005-02-01 paulson 2005-02-01 the new subst tactic, by Lucas Dixon