src/Pure/General/symbol.ML
changeset 61095 50e793295ce1
parent 58864 505a8150368a
child 61435 636bb75e7683