src/Pure/General/symbol.ML
changeset 79946 05e034a54924
parent 77847 3bb6468d202e
child 80797 5d09ceca0924
equal deleted inserted replaced
79945:ca004ccf2352 79946:05e034a54924