src/Pure/attribute.ML
changeset 5526 e7617b57a3e6
parent 5194 650bf0ce0229
child 5559 95e8692fda23