src/Pure/attribute.ML
changeset 5417 1f533238b53b
parent 5194 650bf0ce0229
child 5559 95e8692fda23