src/Pure/General/object.ML
changeset 8413 09db77a084aa
parent 6118 caa439435666
child 8806 a202293db3f6
equal deleted inserted replaced
8412:65f9089f6f71 8413:09db77a084aa