isabelle: File revisions

src/Pure/IsaPlanner/rw_inst.ML

Thu, 02 Jun 2005 09:11:32 +0200	wenzelm	header;	file \| diff \| annotate
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)	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
Fri, 22 Apr 2005 15:10:42 +0200	dixon	lucas - fixed a big with renaming of bound variables. Other small changes.	file \| diff \| annotate
Thu, 21 Apr 2005 19:13:03 +0200	berghofe	Adapted to new interface of instantiation and unification / matching functions.	file \| diff \| annotate
Fri, 04 Mar 2005 15:07:34 +0100	skalberg	Removed practically all references to Library.foldr.	file \| diff \| annotate
Thu, 03 Mar 2005 12:43:01 +0100	skalberg	Move towards standard functions.	file \| diff \| annotate
Wed, 02 Mar 2005 10:33:10 +0100	dixon	lucas - fixed bug with name capture variables bound outside redex could (previously)conflict with scheme variables that occur in the conditions of an equation, and which were renamed to avoid conflict with another instantiation. This has now been fixed.	file \| diff \| annotate
Tue, 01 Feb 2005 18:01:57 +0100	paulson	the new subst tactic, by Lucas Dixon	file \| diff \| annotate

isabelle