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