src/Pure/term_subst.ML
Tue, 12 Sep 2006 12:16:17 +0200 wenzelm Efficient term substitution -- avoids copying.
less more (0) tip