isabelle: File revisions

src/Provers/eqsubst.ML

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	file \| diff \| annotate
Thu, 05 May 2005 13:21:05 +0200	dixon	lucas - added option to select occurance to rewrite e.g. (occ 4)	file \| diff \| annotate
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.	file \| diff \| annotate
Tue, 26 Apr 2005 20:38:39 +0200	dixon	lucas - updated to reflect isand.ML update	file \| diff \| annotate
Fri, 22 Apr 2005 15:10:42 +0200	dixon	lucas - fixed a big with renaming of bound variables. Other small changes.	file \| diff \| annotate
Sun, 27 Feb 2005 00:00:40 +0100	dixon	lucas - added more comments and an extra type to clarify the code.	file \| diff \| annotate
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

isabelle