src/Pure/term_subst.ML
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