src/Provers/eqsubst.ML
Fri, 28 Oct 2005 16:35:40 +0200 haftmann cleaned up nth, nth_update, nth_map and nth_string functions
Sat, 08 Oct 2005 20:15:34 +0200 wenzelm minor tweaks for Poplog/PML;
Mon, 01 Aug 2005 19:20:32 +0200 wenzelm tuned signature;
Fri, 17 Jun 2005 18:33:19 +0200 wenzelm added Id;
Thu, 19 May 2005 01:22:53 +0200 dixon lucas - bugfix to subst in assumptions: fixed index error for conditional rules.
Wed, 18 May 2005 23:04:13 +0200 dixon lucas - fixed subst in assumptions to count redexes from left to right.
Fri, 13 May 2005 20:21:41 +0200 dixon lucas - fixed bug with uninstantiated type contexts in eqsubst and added the automatic removal of duplicate subgoals (when there are no flex-flex constraints)
Fri, 06 May 2005 18:01:44 +0200 dixon lucas - added ability to provide multiple replacements for subst: syntax is now: subst (1 3) myrule
Thu, 05 May 2005 13:21:05 +0200 dixon lucas - added option to select occurance to rewrite e.g. (occ 4)
Tue, 03 May 2005 02:45:55 +0200 dixon lucas - improved interface to isand.ML and cleaned up clean-unification code, and added some better comments.
Tue, 26 Apr 2005 20:38:39 +0200 dixon lucas - updated to reflect isand.ML update
Fri, 22 Apr 2005 15:10:42 +0200 dixon lucas - fixed a big with renaming of bound variables. Other small changes.
Sun, 27 Feb 2005 00:00:40 +0100 dixon lucas - added more comments and an extra type to clarify the code.
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.
Wed, 02 Feb 2005 15:43:04 +0100 paulson improved handling of chained facts
Tue, 01 Feb 2005 18:01:57 +0100 paulson the new subst tactic, by Lucas Dixon
less more (0) tip