src/Pure/General/symbol.ML
changeset 31180 dae7be64d614
parent 31013 69a476d6fea6
child 31425 e8d5417a1831