Sat, 19 Feb 2005 18:44:34 +0100 | dixon | 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. | file | diff | annotate |
Wed, 02 Feb 2005 15:43:04 +0100 | paulson | improved handling of chained facts | file | diff | annotate |
Tue, 01 Feb 2005 18:01:57 +0100 | paulson | the new subst tactic, by Lucas Dixon | file | diff | annotate |