src/Provers/eqsubst.ML
2008-12-31 ago moved term order operations to structure TermOrd (cf. Pure/term_ord.ML);
2008-08-09 ago unified Args.T with OuterLex.token, renamed some operations;
2008-06-01 ago fixed bug: maxidx was wrongly calculuated from term, now calculated
2007-05-21 ago add a bottom up search function
2007-04-18 ago Improved comments.
2007-04-04 ago removed obsolete sign_of/sign_of_thm;
2006-12-18 ago switched argument order in *.syntax lifters
2006-12-07 ago reorganized structure Tactic vs. MetaSimplifier;
2006-11-29 ago simplified method setup;
2006-08-02 ago normalized Proof.context/method type aliases;
2006-07-11 ago replaced Term.variant(list) by Name.variant(_list);
2006-07-03 ago fix to subst in order to allow subst when head of a term is a bound variable.
2006-06-13 ago Corrected search order for zippers.
2006-06-12 ago tuned Seq/Envir/Unify interfaces;
2006-06-11 ago added updated version of IsaPlanner and substitution.
2006-04-26 ago tuned;
2006-02-15 ago used Tactic.distinct_subgoals_tac;
2006-02-10 ago Args/Attrib syntax: Context.generic;
2006-01-29 ago tuned comment;
2006-01-19 ago setup: theory -> theory;
2006-01-06 ago prep_meta_eq: reuse mk_rews of local simpset;
2006-01-06 ago tuned EqSubst setup;
2005-10-28 ago cleaned up nth, nth_update, nth_map and nth_string functions
2005-10-08 ago minor tweaks for Poplog/PML;
2005-08-01 ago tuned signature;
2005-06-17 ago added Id;
2005-05-19 ago lucas - bugfix to subst in assumptions: fixed index error for conditional rules.
2005-05-18 ago lucas - fixed subst in assumptions to count redexes from left to right.
2005-05-13 ago 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 ago lucas - added ability to provide multiple replacements for subst: syntax is now: subst (1 3) myrule
2005-05-05 ago lucas - added option to select occurance to rewrite e.g. (occ 4)
2005-05-03 ago lucas - improved interface to isand.ML and cleaned up clean-unification code, and added some better comments.
2005-04-26 ago lucas - updated to reflect isand.ML update
2005-04-22 ago lucas - fixed a big with renaming of bound variables. Other small changes.
2005-02-27 ago lucas - added more comments and an extra type to clarify the code.
2005-02-19 ago 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 ago improved handling of chained facts
2005-02-01 ago the new subst tactic, by Lucas Dixon