src/Pure/General/symbol.ML
changeset 68669 7ddf297cfcde
parent 67522 9e712280cc37
child 69452 704915cf59fa