src/Pure/General/symbol.ML
changeset 23719 ccd9cb15c062
parent 23682 cf4773532006
child 23728 8409a0cd5b04