src/Pure/General/symbol.ML
changeset 68572 c8bf6077a87d
parent 67522 9e712280cc37
child 69452 704915cf59fa
equal deleted inserted replaced
68568:cf01d04e94d7 68572:c8bf6077a87d