src/Provers/eqsubst.ML
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