src/Pure/old_term.ML
Wed, 31 Dec 2008 00:01:07 +0100 wenzelm Some old-style term operations.
less more (0) tip