src/Provers/eqsubst.ML
2007-04-04 wenzelm 2007-04-04 removed obsolete sign_of/sign_of_thm;
2006-12-18 haftmann 2006-12-18 switched argument order in *.syntax lifters
2006-12-07 wenzelm 2006-12-07 reorganized structure Tactic vs. MetaSimplifier;
2006-11-29 wenzelm 2006-11-29 simplified method setup;
2006-08-02 wenzelm 2006-08-02 normalized Proof.context/method type aliases;
2006-07-11 wenzelm 2006-07-11 replaced Term.variant(list) by Name.variant(_list);
2006-07-03 dixon 2006-07-03 fix to subst in order to allow subst when head of a term is a bound variable.
2006-06-13 dixon 2006-06-13 Corrected search order for zippers.
2006-06-12 wenzelm 2006-06-12 tuned Seq/Envir/Unify interfaces;
2006-06-11 dixon 2006-06-11 added updated version of IsaPlanner and substitution.
2006-04-26 wenzelm 2006-04-26 tuned;
2006-02-15 wenzelm 2006-02-15 used Tactic.distinct_subgoals_tac;
2006-02-10 wenzelm 2006-02-10 Args/Attrib syntax: Context.generic;
2006-01-29 wenzelm 2006-01-29 tuned comment;
2006-01-19 wenzelm 2006-01-19 setup: theory -> theory;
2006-01-06 wenzelm 2006-01-06 prep_meta_eq: reuse mk_rews of local simpset; adapted ML code to common conventions; tuned;
2006-01-06 wenzelm 2006-01-06 tuned EqSubst setup;
2005-10-28 haftmann 2005-10-28 cleaned up nth, nth_update, nth_map and nth_string functions
2005-10-08 wenzelm 2005-10-08 minor tweaks for Poplog/PML;
2005-08-01 wenzelm 2005-08-01 tuned signature;
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