src/Pure/General/symbol.ML
changeset 16465 eb287ce97230
parent 16138 727c5e32930e
child 17063 502105583951
equal deleted inserted replaced
16464:db2711d07cd8 16465:eb287ce97230