src/Pure/attribute.ML
changeset 5545 9117a0e2bf31
parent 5194 650bf0ce0229
child 5559 95e8692fda23