src/Pure/term_subst.ML
2010-05-09 wenzelm 2010-05-09 tuned;
2010-05-09 wenzelm 2010-05-09 removed unused "option" variants of "same" operations;
2010-05-04 wenzelm 2010-05-04 simplified/unified fundamental operations on types/terms/proofterms -- prefer Same.operation over "option" variant;
2010-02-27 wenzelm 2010-02-27 modernized structure Term_Ord;
2009-09-29 wenzelm 2009-09-29 explicit indication of Unsynchronized.ref;
2009-07-16 wenzelm 2009-07-16 use structure Same; tuned;
2009-07-16 wenzelm 2009-07-16 use structure Same; more exports; tuned;
2009-07-10 wenzelm 2009-07-10 added some generic mapping combinators; share private exception SAME locally;
2009-07-09 wenzelm 2009-07-09 renamed structure TermSubst to Term_Subst;
2008-12-31 wenzelm 2008-12-31 moved term order operations to structure TermOrd (cf. Pure/term_ord.ML); tuned signature of structure Term;
2006-11-30 wenzelm 2006-11-30 zero_var_indexes_inst: multiple terms; tuned;
2006-11-12 wenzelm 2006-11-12 instantiate: tuned indentity case;
2006-11-05 wenzelm 2006-11-05 instantiate: avoid global references;
2006-09-12 wenzelm 2006-09-12 Efficient term substitution -- avoids copying. moved here from term.ML; added instantiate_maxidx;