src/Pure/General/object.ML
changeset 5253 82a5ca6290aa
parent 5016 67c5966611c6
child 6118 caa439435666