src/Pure/object.ML
Fri, 05 Jun 1998 14:21:11 +0200 wenzelm added object.ML;
less more (0) tip