src/Pure/General/symbol.ML
changeset 77967 6bb2f9b32804
parent 77847 3bb6468d202e
child 80797 5d09ceca0924
equal deleted inserted replaced
77966:fa3474ed80be 77967:6bb2f9b32804