Wed, 22 Jun 2005 19:41:22 +0200 | wenzelm | renamed init to init_data; | changeset | files |
Wed, 22 Jun 2005 19:41:20 +0200 | wenzelm | added structure Object (from Pure/General/object.ML); | changeset | files |
Wed, 22 Jun 2005 19:41:19 +0200 | wenzelm | tuned; | changeset | files |