src/Pure/General/symbol.ML
changeset 26436 dfd6947ab5c2
parent 25644 d30391cdd9d9
child 26524 63953bec4c98