2005-06-02 wenzelm 2005-06-02 header;
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-03 dixon 2005-05-03 lucas - improved interface to isand.ML and cleaned up clean-unification code, and added some better comments.
2005-04-22 dixon 2005-04-22 lucas - fixed a big with renaming of bound variables. Other small changes.
2005-04-21 berghofe 2005-04-21 Adapted to new interface of instantiation and unification / matching functions.
2005-03-04 skalberg 2005-03-04 Removed practically all references to Library.foldr.
2005-03-03 skalberg 2005-03-03 Move towards standard functions.
2005-03-02 dixon 2005-03-02 lucas - fixed bug with name capture variables bound outside redex could (previously)conflict with scheme variables that occur in the conditions of an equation, and which were renamed to avoid conflict with another instantiation. This has now been fixed.
2005-02-01 paulson 2005-02-01 the new subst tactic, by Lucas Dixon