src/Pure/General/object.ML
Wed, 10 Jun 1998 11:54:04 +0200 wenzelm moved object.ML to General/object.ML;
less more (0) tip