src/Pure/General/object.ML
Fri, 05 May 2000 22:02:46 +0200 wenzelm GPLed;
Wed, 13 Jan 1999 15:18:02 +0100 wenzelm fixed titles;
Wed, 10 Jun 1998 11:54:04 +0200 wenzelm moved object.ML to General/object.ML;
less more (0) tip