src/Pure/General/symbol.ML
changeset 69482 186b03abb764
parent 69452 704915cf59fa
child 69490 ce85542368b9