src/Pure/General/symbol.ML
changeset 69450 b28b001e7ee8
parent 67522 9e712280cc37
child 69452 704915cf59fa