src/Pure/compress.ML
Mon, 01 Aug 2005 19:20:35 +0200 wenzelm compression of terms and types by sharing common subtrees;
less more (0) tip