src/Pure/term_subst.ML
Thu, 30 Nov 2006 14:17:32 +0100 wenzelm zero_var_indexes_inst: multiple terms;
Sun, 12 Nov 2006 21:14:52 +0100 wenzelm instantiate: tuned indentity case;
Sun, 05 Nov 2006 21:44:39 +0100 wenzelm instantiate: avoid global references;
Tue, 12 Sep 2006 12:16:17 +0200 wenzelm Efficient term substitution -- avoids copying.
less more (0) tip