src/Pure/General/object.ML
2000-05-05 wenzelm 2000-05-05 GPLed;
1999-01-13 wenzelm 1999-01-13 fixed titles;
1998-06-10 wenzelm 1998-06-10 moved object.ML to General/object.ML;